ody>
Theory StandardBorel
(* Title: StandardBorel.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) section â¹Standard Borel Spaces⺠theory StandardBorel imports "HOL-Probability.Probability" begin text â¹A standard Borel space is the Borel space associated with a Polish space. Here, we define standard Borel spaces in another, but equivallent, way. See @{cite "Heunen_2017"} Proposition 5. ⺠abbreviation "real_borel â¡ borel :: real measure" abbreviation "nat_borel â¡ borel :: nat measure" abbreviation "ennreal_borel â¡ borel :: ennreal measure" abbreviation "bool_borel â¡ borel :: bool measure" subsection â¹ Definition ⺠locale standard_borel = fixes M :: "'a measure" assumes exist_fg: "âf â M ââ©M real_borel. âg â real_borel ââ©M M. âx â space M. (g â f) x = x" begin abbreviation "fg â¡ (SOME k. (fst k) â M ââ©M real_borel â§ (snd k) â real_borel ââ©M M â§ (âx â space M. ((snd k) â (fst k)) x = x))" definition "f â¡ (fst fg)" definition "g â¡ (snd fg)" lemma shows f_meas[simp,measurable] : "f â M ââ©M real_borel" and g_meas[simp,measurable] : "g â real_borel ââ©M M" and gf_comp_id[simp]: "âx. x â space M â¹ (g â f) x = x" "âx. x â space M â¹ g (f x) = x" proof - obtain f' g' where h: "f' â M ââ©M real_borel" "g' â real_borel ââ©M M" "âx â space M. (g' â f') x = x" using exist_fg by blast have "f â borel_measurable M â§ g â real_borel ââ©M M â§ (âxâspace M. (g â f) x = x)" unfolding f_def g_def by(rule someI2[where a="(f',g')"]) (use h in auto) thus "f â borel_measurable M" "g â real_borel ââ©M M" "âx. x â space M â¹ (g â f) x = x" "âx. x â space M â¹ g (f x) = x" by auto qed lemma standard_borel_sets[simp]: assumes "sets M = sets Y" shows "standard_borel Y" unfolding standard_borel_def using measurable_cong_sets[OF assms refl,of real_borel] measurable_cong_sets[OF refl assms,of real_borel] sets_eq_imp_space_eq[OF assms] exist_fg by simp lemma f_inj: "inj_on f (space M)" by standard (use gf_comp_id(2) in fastforce) lemma singleton_sets: assumes "x â space M" shows "{x} â sets M" proof - let ?y = "f x" let ?U = "f -` {?y}" have "?U â© space M â sets M" using borel_measurable_vimage f_meas by blast moreover have "?U â© space M = {x}" using assms f_inj by(auto simp:inj_on_def) ultimately show ?thesis by simp qed lemma countable_space_discrete: assumes "countable (space M)" shows "sets M = sets (count_space (space M))" proof show "sets (count_space (space M)) â sets M" proof auto fix U assume 1:"U â space M" then have 2:"countable U" using assms countable_subset by auto have 3:"U = (âxâU. {x})" by auto moreover have "... â sets M" by(rule sets.countable_UN''[of U "λx. {x}"]) (use 1 2 singleton_sets in auto) ultimately show "U â sets M" by simp qed qed (simp add: sets.sets_into_space subsetI) end lemma standard_borelI: assumes "f â Y ââ©M real_borel" "g â real_borel ââ©M Y" and "ây. y â space Y â¹ (g â f) y = y" shows "standard_borel Y" unfolding standard_borel_def by (intro bexI[OF _ assms(1)] bexI[OF _ assms(2)]) (auto dest: assms(3)) locale standard_borel_space_UNIV = standard_borel + assumes space_UNIV:"space M = UNIV" begin lemma gf_comp_id'[simp]: "g â f = id" "g (f x) = x" using space_UNIV gf_comp_id by(simp_all add: id_def comp_def) lemma f_inj': "inj f" using f_inj by(simp add: space_UNIV) lemma g_surj': "surj g" using gf_comp_id'(2) surjI by blast end lemma standard_borel_space_UNIVI: assumes "f â Y ââ©M real_borel" "g â real_borel ââ©M Y" "(g â f) = id" and "space Y = UNIV" shows "standard_borel_space_UNIV Y" using assms by(auto intro!: standard_borelI simp: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def) lemma standard_borel_space_UNIVI': assumes "standard_borel Y" and "space Y = UNIV" shows "standard_borel_space_UNIV Y" using assms by(simp add: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def) subsection â¹ $\mathbb{R}$, $\mathbb{N}$, Boolean, $[0,\infty]$ ⺠text â¹ $\mathbb{R}$ is a standard Borel space. ⺠interpretation real : standard_borel_space_UNIV "real_borel" by(auto intro!: standard_borel_space_UNIVI) textâ¹ A non-empty Borel subspace of $\mathbb{R}$ is also a standard Borel space. ⺠lemma real_standard_borel_subset: assumes "U â sets real_borel" and "U â {}" shows "standard_borel (restrict_space real_borel U)" proof - have std1: "id â (restrict_space real_borel U) ââ©M real_borel" by (simp add: measurable_restrict_space1) obtain x where hx : "x â U" using assms(2) by auto define g :: "real â real" where "g â¡ (λr. if r â U then r else x)" have "g â real_borel ââ©M real_borel" unfolding g_def by(rule borel_measurable_continuous_on_if) (simp_all add: assms(1)) hence std2: "g â real_borel ââ©M (restrict_space real_borel U)" by(auto intro!: measurable_restrict_space2 simp: g_def hx) have std3: "âyâ space (restrict_space real_borel U). (g â id) y = y" by(simp add: g_def space_restrict_space) show ?thesis using std1 std2 std3 standard_borel_def by blast qed text â¹ A non-empty measurable subset of a standard Borel space is also a standard Borel space.⺠lemma(in standard_borel) standard_borel_subset: assumes "U â sets M" "U â {}" shows "standard_borel (restrict_space M U)" proof - let ?ginvU = "g -` U" have hgu1:"?ginvU â sets real_borel" using assms(1) g_meas measurable_sets_borel by blast have hgu2:"f ` U â ?ginvU" using gf_comp_id sets.sets_into_space[OF assms(1)] by fastforce hence hgu3:"?ginvU â {}" using assms(2) by blast interpret r_borel_set: standard_borel "restrict_space real_borel ?ginvU" by(rule real_standard_borel_subset[OF hgu1 hgu3]) have std1: "r_borel_set.f â f â (restrict_space M U) ââ©M real_borel" using sets.sets_into_space[OF assms(1)] by(auto intro!: measurable_comp[where N="restrict_space real_borel ?ginvU"] measurable_restrict_space3) have std2: "g â r_borel_set.g â real_borel ââ©M (restrict_space M U)" by(auto intro!: measurable_comp[where N="restrict_space real_borel ?ginvU"] measurable_restrict_space3[OF g_meas]) have std3: "âxâ space (restrict_space M U). ((g â r_borel_set.g) â (r_borel_set.f â f)) x = x" by (simp add: space_restrict_space) show ?thesis using std1 std2 std3 standard_borel_def by blast qed text â¹ $\mathbb{N}$ is a standard Borel space. ⺠interpretation nat : standard_borel_space_UNIV nat_borel proof - define n_to_r :: "nat â real" where "n_to_r â¡ (λn. of_real n)" define r_to_n :: "real â nat" where "r_to_n â¡ (λr. nat ârâ)" have n_to_r_measurable: "n_to_r â nat_borel ââ©M real_borel" using borel_measurable_count_space measurable_cong_sets sets_borel_eq_count_space by blast have r_to_n_measurable: "r_to_n â real_borel ââ©M nat_borel" by(simp add: r_to_n_def) have n_to_r_to_n_id: "r_to_n â n_to_r = id" by(simp add: n_to_r_def r_to_n_def comp_def id_def) show "standard_borel_space_UNIV nat_borel" using standard_borel_space_UNIVI[OF n_to_r_measurable r_to_n_measurable n_to_r_to_n_id] by simp qed text â¹ For a countable space $X$, $X$ is a standard Borel space iff $X$ is a discrete space. ⺠lemma countable_standard_iff: assumes "space X â {}" and "countable (space X)" shows "standard_borel X â· sets X = sets (count_space (space X))" proof show "standard_borel X â¹ sets X = sets (count_space (space X))" using standard_borel.countable_space_discrete assms by simp next assume h[measurable_cong]: "sets X = sets (count_space (space X))" show "standard_borel X" proof(rule standard_borelI[where f="nat.f â to_nat_on (space X)" and g="from_nat_into (space X) â nat.g"]) show "nat.f â to_nat_on (space X) â borel_measurable X" by simp next have [simp]: "from_nat_into (space X) â UNIV â (space X)" using from_nat_into[OF assms(1)] by simp hence [measurable]: "from_nat_into (space X) â nat_borel ââ©M X" using measurable_count_space_eq1[of _ _ X] measurable_cong_sets[OF sets_borel_eq_count_space] by blast show "from_nat_into (space X) â nat.g â real_borel ââ©M X" by simp next fix x assume "x â space X" then show "(from_nat_into (space X) â nat.g â (nat.f â to_nat_on (space X))) x = x" using from_nat_into_to_nat_on[OF assms(2)] by simp qed qed text â¹ $\mathbb{B}$ is a standard Borel space. ⺠lemma to_bool_measurable: assumes "f -` {True} â© space M â sets M" shows "f â M ââ©M bool_borel" proof(rule measurableI) fix A assume h:"A â sets bool_borel" have h2: "f -` {False} â© space M â sets M" proof - have "- {False} = {True}" by auto thus ?thesis by(simp add: vimage_sets_compl_iff[where A="{False}"] assms) qed have "A â {True,False}" by auto then consider "A = {}" | "A = {True}" | "A = {False}" | "A = {True,False}" by auto thus "f -` A â© space M â sets M" proof cases case 1 then show ?thesis by simp next case 2 then show ?thesis by(simp add: assms) next case 3 then show ?thesis by(simp add: h2) next case 4 then have "f -` A = f -` {True} ⪠f -` {False}" by auto thus ?thesis using assms h2 by (metis Int_Un_distrib2 sets.Un) qed qed simp interpretation bool : standard_borel_space_UNIV bool_borel using countable_standard_iff[of bool_borel] by(auto intro!: standard_borel_space_UNIVI' simp: sets_borel_eq_count_space) text â¹ $[0,\infty]$ (the set of extended non-negative real numbers) is a standard Borel space. ⺠interpretation ennreal : standard_borel_space_UNIV ennreal_borel proof - define preal_to_real :: "ennreal â real" where "preal_to_real â¡ (λr. if r = â then -1 else enn2real r)" define real_to_preal :: "real â ennreal" where "real_to_preal â¡ (λr. if r = -1 then â else ennreal r)" have preal_to_real_measurable: "preal_to_real â ennreal_borel ââ©M real_borel" unfolding preal_to_real_def by simp have real_to_preal_measurable: "real_to_preal â real_borel ââ©M ennreal_borel" unfolding real_to_preal_def by simp have preal_real_preal_id: "real_to_preal â preal_to_real = id" proof fix r :: ennreal show "(real_to_preal â preal_to_real) r = id r" using ennreal_enn2real_if[of r] ennreal_neg by(auto simp add: real_to_preal_def preal_to_real_def) qed show "standard_borel_space_UNIV ennreal_borel" using standard_borel_space_UNIVI[OF preal_to_real_measurable real_to_preal_measurable preal_real_preal_id] by simp qed subsection â¹ $\mathbb{R}\times\mathbb{R}$ ⺠definition real_to_01open :: "real â real" where "real_to_01open r â¡ arctan r / pi + 1 / 2" definition real_to_01open_inverse :: "real â real" where "real_to_01open_inverse r â¡ tan (pi * r - (pi / 2))" lemma real_to_01open_inverse_correct: "real_to_01open_inverse â real_to_01open = id" by(auto simp add: real_to_01open_def real_to_01open_inverse_def distrib_left tan_arctan) lemma real_to_01open_inverse_correct': assumes "0 < r" "r < 1" shows "real_to_01open (real_to_01open_inverse r) = r" unfolding real_to_01open_def real_to_01open_inverse_def proof - have "arctan (tan (pi * r - pi / 2)) = pi * r - pi / 2" using arctan_unique[of "pi * r - pi / 2"] assms by simp hence "arctan (tan (pi * r - pi / 2)) / pi + 1 / 2 = ((pi * r) - pi / 2)/ pi + 1/2" by simp also have "... = r - 1/2 + 1/2" by (metis (no_types, opaque_lifting) divide_inverse mult.left_neutral nonzero_mult_div_cancel_left pi_neq_zero right_diff_distrib) finally show "arctan (tan (pi * r - pi / 2)) / pi + 1 / 2 = r" by simp qed lemma real_to_01open_01 : "0 < real_to_01open r â§ real_to_01open r < 1" proof have "- pi / 2 < arctan r" by(simp add: arctan_lbound) hence "0 < arctan r + pi / 2" by simp hence "0 < (1 / pi) * (arctan r + pi / 2)" by simp thus "0 < real_to_01open r" by (simp add: add_divide_distrib real_to_01open_def) next have "arctan r < pi / 2" using arctan_ubound by simp hence "arctan r + pi / 2 < pi" by simp hence "(1 / pi) * (arctan r + pi / 2) < 1" by simp thus "real_to_01open r < 1" by(simp add: real_to_01open_def add_divide_distrib) qed lemma real_to_01open_continuous: "continuous_on UNIV real_to_01open" proof - have "continuous_on UNIV ((λx. x / pi + 1 / 2) â arctan)" proof (rule continuous_on_compose) show "continuous_on UNIV arctan" by (simp add: continuous_on_arctan) next show "continuous_on (range arctan) (λx. x / pi + 1 / 2)" by(auto intro!: continuous_on_add continuous_on_divide) qed thus ?thesis by(simp add: real_to_01open_def) qed lemma real_to_01open_inverse_continuous: "continuous_on {0<..<1} real_to_01open_inverse" unfolding real_to_01open_inverse_def proof(rule Transcendental.continuous_on_tan) have [simp]: "(λx. pi * x - pi / 2) = (λx. x - pi/2) â (λx. pi * x)" by auto have "continuous_on {0<..<1} ..." proof(rule continuous_on_compose) show "continuous_on {0<..<1} ((*) pi)" by simp next show "continuous_on ((*) pi ` {0<..<1}) (λx. x - pi / 2)" using continuous_on_diff[of "(*) pi ` {0<..<1}" "λx. x"] by simp qed thus "continuous_on {0<..<1} (λx. pi * x - pi / 2)" by simp next have "ârâ{0<..<1::real}. -(pi/2) < pi * r - pi / 2 â§ pi * r - pi / 2 < pi/2" by simp thus "ârâ{0<..<1::real}. cos (pi * r - pi / 2) â 0" using cos_gt_zero_pi by fastforce qed lemma real_to_01open_inverse_measurable: "real_to_01open_inverse â restrict_space real_borel {0<..<1} ââ©M real_borel" using borel_measurable_continuous_on_restrict real_to_01open_inverse_continuous by simp fun r01_binary_expansion'' :: "real â nat â nat à real à real" where "r01_binary_expansion'' r 0 = (if 1/2 ⤠r then (1,1 ,1/2) else (0,1/2, 0))" | "r01_binary_expansion'' r (Suc n) = (let (_,ur,lr) = r01_binary_expansion'' r n; k = (ur + lr)/2 in (if k ⤠r then (1,ur,k) else (0,k,lr)))" text â¹ $a_n$ where $r = 0.a_0 a_1 a_2 ....$ for $0 < r < 1$.⺠definition r01_binary_expansion' :: "real â nat â nat" where "r01_binary_expansion' r n â¡ fst (r01_binary_expansion'' r n)" text â¹$a_n = 0$ or $1$.⺠lemma real01_binary_expansion'_0or1: "r01_binary_expansion' r n â {0,1}" by (cases n) (simp_all add: r01_binary_expansion'_def split_beta' Let_def) (* S_n = a_0 + ... + a_n *) definition r01_binary_sum :: "(nat â nat) â nat â real" where "r01_binary_sum a n â¡ (âi=0..n. real (a i) * ((1/2)^(Suc i)))" definition r01_binary_sum_lim :: "(nat â nat) â real" where "r01_binary_sum_lim â¡ lim â r01_binary_sum" definition r01_binary_expression :: "real â nat â real" where "r01_binary_expression â¡ r01_binary_sum â r01_binary_expansion'" lemma r01_binary_expansion_lr_r_ur: assumes "0 < r" "r < 1" shows "(snd (snd (r01_binary_expansion'' r n))) ⤠r â§ r < (fst (snd (r01_binary_expansion'' r n)))" using assms by (induction n) (simp_all add:split_beta' Let_def) text â¹â¹0 ⤠lr â§ lr < ur â§ ur ⤠1âº.⺠lemma r01_binary_expansion_lr_ur_nn: shows "0 ⤠snd (snd (r01_binary_expansion'' r n)) â§ snd (snd (r01_binary_expansion'' r n)) < fst (snd (r01_binary_expansion'' r n)) â§ fst (snd (r01_binary_expansion'' r n)) ⤠1" by (induction n) (simp_all add:split_beta' Let_def) lemma r01_binary_expansion_diff: shows "(fst (snd (r01_binary_expansion'' r n))) - (snd (snd (r01_binary_expansion'' r n))) = (1/2)^(Suc n)" proof(induction n) case (Suc n') then show ?case proof(cases "r01_binary_expansion'' r n'") case 1:(fields a ur lr) assume "fst (snd (r01_binary_expansion'' r n')) - snd (snd (r01_binary_expansion'' r n')) = (1 / 2) ^ (Suc n')" then have 2:"ur - lr = (1/2)^(Suc n')" by (simp add: 1) show ?thesis proof - have [simp]:"ur * 4 - (ur * 4 + lr * 4) / 2 = (ur - lr) * 2" by(simp add: division_ring_class.add_divide_distrib) have "ur * 4 - (ur * 4 + lr * 4) / 2 = (1 / 2) ^ n'" by(simp add: 2) moreover have "(ur * 4 + lr * 4) / 2 - lr * 4 = (1 / 2) ^ n'" by(simp add: division_ring_class.add_divide_distrib ring_class.right_diff_distrib[symmetric] 2) ultimately show ?thesis by(simp add: 1 Let_def) qed qed qed simp text â¹â¹lrn = Snâº.⺠lemma r01_binary_expression_eq_lr: "snd (snd (r01_binary_expansion'' r n)) = r01_binary_expression r n" proof(induction n) case 0 then show ?case by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def) next case 1:(Suc n') show ?case proof (cases "r01_binary_expansion'' r n'") case 2:(fields a ur lr) then have ih:"lr = (âi = 0..n'. real (fst (r01_binary_expansion'' r i)) * (1 / 2) ^ i / 2)" using 1 by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def) have 3:"(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n'))" using r01_binary_expansion_diff[of r n'] 2 by simp show ?thesis by(simp add: r01_binary_expression_def r01_binary_sum_def r01_binary_expansion'_def 2 Let_def 3) fact qed qed lemma r01_binary_expression'_sum_range: "âk::nat. (snd (snd (r01_binary_expansion'' r n))) = real k/2^(Suc n) â§ k < 2^(Suc n) â§ ((r01_binary_expansion' r n) = 0 â¶ even k) â§ ((r01_binary_expansion' r n) = 1 â¶ odd k)" proof - have [simp]:"(snd (snd (r01_binary_expansion'' r n))) = (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i)))" using r01_binary_expression_eq_lr[of r n] by(simp add: r01_binary_expression_def r01_binary_sum_def) have "âk::nat. (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) = real k/2^(Suc n) â§ k < 2^(Suc n) â§ ((r01_binary_expansion' r n) = 0 â¶ even k) â§ ((r01_binary_expansion' r n) = 1 â¶ odd k)" proof(induction n) case 0 consider "r01_binary_expansion' r 0 = 0" | "r01_binary_expansion' r 0 = 1" using real01_binary_expansion'_0or1[of r 0] by auto then show ?case by cases auto next case (Suc n') then obtain k :: nat where ih: "(âi = 0..n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = real k / 2^(Suc n') â§ k < 2^(Suc n')" by auto have "(âi = 0..Suc n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = (âi = 0..n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) + real (r01_binary_expansion' r (Suc n')) * (1 / 2) ^ Suc (Suc n')" by simp also have "... = real k / 2^(Suc n') + (real (r01_binary_expansion' r (Suc n')))/ 2^ Suc (Suc n')" proof - have "âr ra n. (r::real) * (1 / ra) ^ n = r / ra ^ n" by (simp add: power_one_over) then show ?thesis using ih by presburger qed also have "... = (2*real k) / 2^(Suc (Suc n')) + (real (r01_binary_expansion' r (Suc n')))/ 2^ Suc (Suc n')" by simp also have "... = (2*(real k) + real (r01_binary_expansion' r (Suc n')))/2 ^ Suc (Suc n')" by (simp add: add_divide_distrib) also have "... = (real (2*k + r01_binary_expansion' r (Suc n')))/2 ^ Suc (Suc n')" by simp finally have "(âi = 0..Suc n'. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) = real (2 * k + r01_binary_expansion' r (Suc n')) / 2 ^ Suc (Suc n')" . moreover have "2 * k + r01_binary_expansion' r (Suc n') < 2^Suc (Suc n')" proof - have "k + 1 ⤠2^Suc n'" using ih by simp hence "2*k + 2 ⤠2^Suc (Suc n')" by simp thus ?thesis using real01_binary_expansion'_0or1[of r "Suc n'"] by auto qed moreover have "r01_binary_expansion' r (Suc n') = 0 â¶ even (2 * k + r01_binary_expansion' r (Suc n'))" by simp moreover have "r01_binary_expansion' r (Suc n') = 1 â¶ odd (2 * k + r01_binary_expansion' r (Suc n'))" by simp ultimately show ?case by fastforce qed thus ?thesis by simp qed text â¹â¹an = bn â Sn = S'nâº.⺠lemma r01_binary_expansion'_expression_eq: "r01_binary_expansion' r1 = r01_binary_expansion' r2 â· r01_binary_expression r1 = r01_binary_expression r2" proof assume "r01_binary_expansion' r1 = r01_binary_expansion' r2" then show "r01_binary_expression r1 = r01_binary_expression r2" by(simp add: r01_binary_expression_def) next assume "r01_binary_expression r1 = r01_binary_expression r2" then have 1:"ân. r01_binary_sum (r01_binary_expansion' r1) n = r01_binary_sum (r01_binary_expansion' r2) n" by(simp add: r01_binary_expression_def) show "r01_binary_expansion' r1 = r01_binary_expansion' r2" proof fix n show " r01_binary_expansion' r1 n = r01_binary_expansion' r2 n" proof(cases n) case 0 then show ?thesis using 1[of 0] by(simp add: r01_binary_sum_def) next fix n' case (Suc n') have "r01_binary_sum (r01_binary_expansion' r1) n - r01_binary_sum (r01_binary_expansion' r1) n' = r01_binary_sum (r01_binary_expansion' r2) n - r01_binary_sum (r01_binary_expansion' r2) n'" by(simp add: 1) thus ?thesis using â¹n = Suc n'⺠by(simp add: r01_binary_sum_def) qed qed qed lemma power2_e: "âe::real. 0 < e â¹ ân::nat. real_of_rat (1/2)^n < e" by (simp add: real_arch_pow_inv) lemma r01_binary_expression_converges_to_r: assumes "0 < r" and "r < 1" shows "LIMSEQ (r01_binary_expression r) r" proof fix e :: real assume "0 < e" then obtain k :: nat where hk:"real_of_rat (1/2)^k < e" using power2_e by auto show "ââ©F x in sequentially. dist (r01_binary_expression r x) r < e" proof(rule eventually_sequentiallyI[of k]) fix m assume "k ⤠m" have "¦ r - r01_binary_expression r m ¦ < e" proof (cases "r01_binary_expansion'' r m") case 1:(fields a ur lr) then have "¦r - r01_binary_expression r m¦ = ¦r - lr¦" by (metis r01_binary_expression_eq_lr snd_conv) also have "... = r - lr" using r01_binary_expansion_lr_r_ur[OF assms] 1 by (metis abs_of_nonneg diff_ge_0_iff_ge snd_conv) also have "... < e" proof - have "r - lr ⤠ur - lr" using r01_binary_expansion_lr_r_ur[of r] assms 1 by (metis diff_right_mono fst_conv less_imp_le snd_conv) also have "... = (1/2)^(Suc m)" using r01_binary_expansion_diff[of r m] by(simp add: 1) also have "... ⤠(1/2)^(Suc k)" using â¹k ⤠m⺠by simp also have "... < (1/2)^k" by simp finally show ?thesis using hk by (simp add: of_rat_divide) qed finally show ?thesis . qed then show "dist (r01_binary_expression r m) r < e" by (simp add: dist_real_def) qed qed lemma r01_binary_expression_correct: assumes "0 < r" and "r < 1" shows "r = (ân. real (r01_binary_expansion' r n) * (1/2)^(Suc n))" proof - have "(λn. (λn. âi<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) (Suc n)) = r01_binary_expression r" proof - have "ân. {..<Suc n} = {0..n}" by auto thus ?thesis by(auto simp add: r01_binary_expression_def r01_binary_sum_def) qed hence "LIMSEQ (λn. âi<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i) r" using r01_binary_expression_converges_to_r[OF assms] LIMSEQ_imp_Suc[of "λn. âi<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i" r] by simp thus ?thesis using suminf_eq_lim[of "λn. real (r01_binary_expansion' r n) * (1/2)^(Suc n)"] assms limI[of "(λn. âi<n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i)" r] by simp qed text â¹â¹S0 ⤠S1 ⤠S2 ⤠...âº.⺠lemma binary_sum_incseq: "incseq (r01_binary_sum a)" by(simp add: incseq_Suc_iff r01_binary_sum_def) lemma r01_eq_iff: assumes "0 < r1" "r1 < 1" "0 < r2" "r2 < 1" shows "r1 = r2 â· r01_binary_expansion' r1 = r01_binary_expansion' r2" proof auto assume "r01_binary_expansion' r1 = r01_binary_expansion' r2" then have 1:"r01_binary_expression r1 = r01_binary_expression r2" using r01_binary_expansion'_expression_eq[of r1 r2] by simp have "r1 = lim (r01_binary_expression r1)" using limI[of _ r1] r01_binary_expression_converges_to_r[of r1] assms(1,2) by simp also have "... = lim (r01_binary_expression r2)" by (simp add: 1) also have "... = r2" using limI[of _ r2] r01_binary_expression_converges_to_r[of r2] assms(3,4) by simp finally show "r1 = r2" . qed lemma power_half_summable: "summable (λn. ((1::real) / 2) ^ Suc n)" using power_half_series summable_def by blast lemma binary_expression_summable: assumes "ân. a n â {0,1 :: nat}" shows "summable (λn. real (a n) * (1/2)^(Suc n))" proof - have "summable (λn::nat. ¦real (a n) * ((1::real) / (2::real)) ^ Suc n¦)" proof(rule summable_rabs_comparison_test[of "λn. real (a n) * (1/2)^(Suc n)" "λn. (1/2)^(Suc n)"]) have "ân. ¦real (a n) * (1 / 2) ^ Suc n¦ ⤠(1 / 2)^(Suc n)" proof - fix n have "¦real (a n) * (1 / 2) ^ Suc n¦ = real (a n) * (1 / 2) ^ Suc n" using assms by simp also have "... ⤠(1 / 2) ^ Suc n" proof - consider "a n = 0" | "a n = 1" using assms by (meson insertE singleton_iff) then show ?thesis by(cases,auto) qed finally show "¦real (a n) * (1 / 2) ^ Suc n¦ ⤠(1 / 2)^(Suc n)" . qed thus "âN. ânâ¥N. ¦real (a n) * (1 / 2) ^ Suc n¦ ⤠(1 / 2) ^ Suc n" by simp next show "summable (λn. ((1::real) / 2) ^ Suc n)" using power_half_summable by simp qed thus ?thesis by simp qed lemma binary_expression_gteq0: assumes "ân. a n â {0,1 :: nat}" shows "0 ⤠(ân. real (a (n + k)) * (1 / 2) ^ Suc (n + k))" proof - have "(ân. 0) ⤠(ân. real (a (n + k)) * (1 / 2) ^ Suc (n + k))" using binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] suminf_le[of "λn. 0" "λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k)"] assms by simp thus ?thesis by simp qed lemma binary_expression_leeq1: assumes "ân. a n â {0,1 :: nat}" shows "(ân. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ⤠1" proof - have "(ân. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ⤠(ân. (1/2)^(Suc n))" proof(rule suminf_le) fix n have 1:"real (a (n + k)) * (1 / 2) ^ Suc (n + k) ⤠(1 / 2) ^ Suc (n + k)" using assms[of "n+k"] by auto have 2:"((1::real) / 2) ^ Suc (n + k) ⤠(1 / 2) ^ Suc n" by simp show "real (a (n + k)) * (1 / 2) ^ Suc (n + k) ⤠(1 / 2) ^ Suc n" by(rule order.trans[OF 1 2]) next show "summable (λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k))" using binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] assms by simp next show "summable (λn. ((1::real) / 2) ^ Suc n)" using power_half_summable by simp qed thus ?thesis using power_half_series sums_unique by fastforce qed lemma binary_expression_less_than: assumes "ân. a n â {0,1 :: nat}" shows "(ân. real (a (n + k)) * (1 / 2) ^ Suc (n + k)) ⤠(ân. (1 / 2) ^ Suc (n + k))" proof(rule suminf_le) fix n show "real (a (n + k)) * (1 / 2) ^ Suc (n + k) ⤠(1 / 2) ^ Suc (n + k)" using assms[of "n + k"] by auto next show "summable (λn. real (a (n + k)) * (1 / 2) ^ Suc (n + k))" using summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" k] binary_expression_summable[of a] assms by simp next show "summable (λn. ((1::real) / 2) ^ Suc (n + k))" using power_half_summable summable_iff_shift[of "λn. ((1::real) / 2) ^ Suc n" k] by simp qed lemma lim_sum_ai: assumes "ân. a n â {0,1 :: nat}" shows "lim (λn. (âi=0..n. real (a i) * (1/2)^(Suc i))) = (ân::nat. real (a n) * (1/2)^(Suc n))" proof - have "ân::nat. {0..n} = {..n}" by auto hence "LIMSEQ (λn. âi=0..n. real (a i) * (1 / 2) ^ Suc i) (ân. real (a n) * (1 / 2) ^ Suc n)" using summable_LIMSEQ'[of "λn. real (a n) * (1/2)^(Suc n)"] binary_expression_summable[of a] assms by simp thus "lim (λn. (âi=0..n. real (a i) * (1/2)^(Suc i))) = (ân. real (a n) * (1 / 2) ^ Suc n)" using limI by simp qed lemma half_1_minus_sum: "1 - (âi<k. ((1::real) / 2) ^ Suc i) = (1/2)^k" by(induction k) auto lemma half_sum: "(ân. ((1::real) / 2) ^ (Suc (n + k))) = (1/2)^k" using suminf_split_initial_segment[of "λn. ((1::real) / 2) ^ (Suc n)" k] half_1_minus_sum[of k] power_half_series sums_unique[of "λn. (1 / 2) ^ Suc n" 1] power_half_summable by fastforce lemma ai_exists0_less_than_sum: assumes "ân. a n â {0,1}" "i ⥠m" and "a i = 0" shows "(ân::nat. real (a (n + m)) * (1/2)^(Suc (n + m))) < (1 / 2) ^ m" proof - have "(ân::nat. real (a (n + m)) * (1/2)^(Suc (n + m))) = (ân<i-m. real (a (n + m)) * (1/2)^(Suc (n + m))) + (ân::nat. real (a (n + i)) * (1/2)^(Suc (n + i)))" using suminf_split_initial_segment[of "λn. real (a (n + m)) * (1/2)^(Suc (n + m))" "i-m"] assms(1) binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" m] assms(2) by simp also have "... < (1 / 2) ^ m" proof - have "(ân. real (a (n + i)) * (1 / 2) ^ Suc (n + i)) ⤠(1 / 2) ^ Suc i" proof - have "(ân::nat. real (a (n + i)) * (1/2)^(Suc (n + i))) = (ân::nat. real (a (Suc n + i)) * (1/2)^(Suc (Suc n + i)))" using suminf_split_head[of "λn. real (a (n + i)) * (1/2)^(Suc (n + i))"] assms(1,3) binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" i] by simp also have "... = (ân::nat. real (a (n + Suc i)) * (1/2)^(Suc n + Suc i))" by simp also have "... ⤠(ân::nat. (1/2)^(Suc n + Suc i))" using binary_expression_less_than[of a "Suc i"] assms(1) by simp also have "... = (1/2)^(Suc i)" using half_sum[of "Suc i"] by simp finally show ?thesis . qed moreover have "(ân<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) ⤠(1/2)^m - (1/2)^i" proof - have "(ân<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) ⤠(ân<i - m. (1 / 2) ^ Suc (n + m))" proof - have "real (a i) * (1 / 2) ^ Suc i ⤠(1 / 2) ^ Suc i" for i using assms(1)[of i] by auto thus ?thesis by (simp add: sum_mono) qed also have "... = (ân. (1 / 2) ^ Suc (n + m)) - (ân. (1 / 2) ^ Suc (n + (i - m) + m))" using suminf_split_initial_segment[of "λn. (1 / 2) ^ Suc (n + m)" "i-m"] power_half_summable summable_iff_shift[of "λn. ((1::real) / 2) ^ Suc n" m] by fastforce also have "... = (ân. (1 / 2) ^ Suc (n + m)) - (ân. (1 / 2) ^ Suc (n + i))" using assms(2) by simp also have "... = (1/2)^m - (1/2)^i" using half_sum by fastforce finally show ?thesis . qed ultimately have "(ân<i - m. real (a (n + m)) * (1 / 2) ^ Suc (n + m)) + (ân. real (a (n + i)) * (1 / 2) ^ Suc (n + i)) ⤠(1 / 2) ^ Suc i + (1 / 2) ^ m - (1 / 2) ^ i" by linarith also have "... < (1 / 2) ^ m " by simp finally show ?thesis . qed finally show ?thesis . qed lemma ai_exists0_less_than1: assumes "ân. a n â {0,1}" and "âi. a i = 0" shows "(ân::nat. real (a n) * (1/2)^(Suc n)) < 1" using ai_exists0_less_than_sum[of a 0] assms by auto lemma ai_1_gt: assumes "ân. a n â {0,1}" and "a i = 1" shows "(1/2)^(Suc i) ⤠(ân::nat. real (a (n+i)) * (1/2)^(Suc (n+i)))" proof - have 1:"(ân::nat. real (a (n+i)) * (1/2)^(Suc (n+i))) = (1 / 2) ^ Suc (0 + i) + (ân. real (a (Suc n + i)) * (1 / 2) ^ Suc (Suc n + i))" using suminf_split_head[of "λn. real (a (n+i)) * (1/2)^(Suc (n+i))"] binary_expression_summable[of a] summable_iff_shift[of "λn. real (a n) * (1 / 2) ^ Suc n" i] assms by simp show ?thesis using 1 binary_expression_gteq0[of a "Suc i"] assms(1) by simp qed lemma ai_exists1_gt0: assumes "ân. a n â {0,1}" and "âi. a i = 1" shows "0 < (ân::nat. real (a n) * (1/2)^(Suc n))" proof - obtain k where h1: "a k = 1" using assms(2) by auto have "(1/2)^(Suc k) = (ân::nat. (if n = k then (1/2)^(Suc k) else (0::real)))" proof - have "(λn. if n â {k} then (1 / 2) ^ Suc k else (0::real)) = (λn. if n = k then (1/2)^(Suc k) else 0)" by simp moreover have "(λn. if n â {k} then (1 / 2) ^ Suc k else (0::real)) sums (ârâ{k}. (1 / 2) ^ Suc k)" using sums_If_finite_set[of "{k}" "λn. ((1::real)/2)^(Suc k)"] by simp ultimately have "(λn. if n = k then (1 / 2) ^ Suc k else (0::real)) sums (1/2)^(Suc k)" by simp thus ?thesis using sums_unique[of "λn. if n = k then (1 / 2) ^ Suc k else (0::real)" "(1/2)^(Suc k)"] by simp qed also have "(ân::nat. (if n = k then (1/2)^(Suc k) else 0)) ⤠(ân::nat. real (a n) * (1/2)^(Suc n))" proof(rule suminf_le) show "ân. (if n = k then (1 / 2) ^ Suc k else 0) ⤠real (a n) * (1 / 2) ^ Suc n" proof - fix n show "(if n = k then (1 / 2) ^ Suc k else 0) ⤠real (a n) * (1 / 2) ^ Suc n" by(cases "n = k"; simp add: h1) qed next show "summable (λn. if n = k then (1 / 2) ^ Suc k else (0::real))" using summable_single[of k "λn. ((1::real) / 2) ^ Suc k"] by simp next show "summable (λn. real (a n) * (1 / 2) ^ Suc n)" using binary_expression_summable[of a] assms(1) by simp qed finally have "(1 / 2) ^ Suc k ⤠(ân. real (a n) * (1 / 2) ^ Suc n)" . moreover have "0 < ((1::real) / 2) ^ Suc k" by simp ultimately show ?thesis by linarith qed lemma r01_binary_expression_ex0: assumes "0 < r" "r < 1" shows "âi. r01_binary_expansion' r i = 0" proof (rule ccontr) assume "¬ (â i. r01_binary_expansion' r i = 0)" then have "âi. r01_binary_expansion' r i = 1" using real01_binary_expansion'_0or1[of r] by blast hence 1:"r01_binary_expression r = (λn. âi=0..n. ((1/2)^(Suc i)))" by(auto simp: r01_binary_expression_def r01_binary_sum_def) have "LIMSEQ (r01_binary_expression r) 1" proof - have "LIMSEQ (λn. âi=0..n. (((1::real)/2)^(Suc i))) 1" using power_half_series sums_def'[of "λn. ((1::real)/2)^(Suc n)" 1] by simp thus ?thesis using 1 by simp qed moreover have "LIMSEQ (r01_binary_expression r) r" using r01_binary_expression_converges_to_r[of r] assms by simp ultimately have "r = 1" using LIMSEQ_unique by auto thus False using assms by simp qed lemma r01_binary_expression_ex1: assumes "0 < r" "r < 1" shows "âi. r01_binary_expansion' r i = 1" proof (rule ccontr) assume "¬ (âi. r01_binary_expansion' r i = 1)" then have "âi. r01_binary_expansion' r i = 0" using real01_binary_expansion'_0or1[of r] by blast hence 1:"r01_binary_expression r = (λn. âi=0..n. 0)" by(auto simp add: r01_binary_expression_def r01_binary_sum_def) hence "LIMSEQ (r01_binary_expression r) 0" by simp moreover have "LIMSEQ (r01_binary_expression r) r" using r01_binary_expression_converges_to_r[of r] assms by simp ultimately have "r = 0" using LIMSEQ_unique by auto thus False using assms by simp qed lemma r01_binary_expansion'_gt1: "1 ⤠r â· (ân. r01_binary_expansion' r n = 1)" proof auto fix n assume h:"1 ⤠r" show "r01_binary_expansion' r n = Suc 0" unfolding r01_binary_expansion'_def proof(cases n) case 0 then show "fst (r01_binary_expansion'' r n) = Suc 0" using h by simp next case 2:(Suc n') show "fst (r01_binary_expansion'' r n) = Suc 0" proof(cases "r01_binary_expansion'' r n'") case 3:(fields a ur lr) then have "(ur + lr) / 2 ⤠1" using r01_binary_expansion_lr_ur_nn[of r "Suc n'"] by (cases "((ur + lr) / 2) ⤠r") (auto simp: Let_def) thus "fst (r01_binary_expansion'' r n) = Suc 0" using h by(simp add: 2 3 Let_def) qed qed next assume h:"ân. r01_binary_expansion' r n = Suc 0" show "1 ⤠r" proof(rule ccontr) assume "¬ 1 ⤠r" then consider "r ⤠0" | "0 < r â§ r < 1" by linarith then show "False" proof cases case 1 then have "r01_binary_expansion' r 0 = 0" by(simp add: r01_binary_expansion'_def) then show ?thesis using h by simp next case 2 then have "âi. r01_binary_expansion' r i = 0" using r01_binary_expression_ex0[of r] by simp then show ?thesis using h by simp qed qed qed lemma r01_binary_expansion'_lt0: "r ⤠0 â· (ân. r01_binary_expansion' r n = 0)" proof auto fix n assume h:"r ⤠0" show "r01_binary_expansion' r n = 0" proof(cases n) case 0 then show ?thesis using h by(simp add: r01_binary_expansion'_def) next case hn:(Suc n') then show ?thesis unfolding r01_binary_expansion'_def proof(cases "r01_binary_expansion'' r n'") case 1:(fields a ur lr) then have "0 < ((ur + lr) / 2)" using r01_binary_expansion_lr_ur_nn[of r n'] by simp hence "r < ..." using h by linarith then show "fst (r01_binary_expansion'' r n) = 0 " by(simp add: 1 hn Let_def) qed qed next assume h:"ân. r01_binary_expansion' r n = 0" show "r ⤠0" proof(rule ccontr) assume "¬ r ⤠0" then consider "0 < r â§ r < 1" | "1 ⤠r" by linarith thus False proof cases case 1 then have "âi. r01_binary_expansion' r i = 1" using r01_binary_expression_ex1[of r] by simp then show ?thesis using h by simp next case 2 then show ?thesis using r01_binary_expansion'_gt1[of r] h by simp qed qed qed text â¹The sequence $111111\dots$ does not appear in $r = 0.a_1 a_2\dots$. ⺠lemma r01_binary_expression_ex0_strong: assumes "0 < r" "r < 1" shows "âiâ¥n. r01_binary_expansion' r i = 0" proof(cases "r01_binary_expansion'' r n") case 1:(fields a ur lr) show ?thesis proof(rule ccontr) assume "¬ (âiâ¥n. r01_binary_expansion' r i = 0)" then have h:"âiâ¥n. r01_binary_expansion' r i = 1" using real01_binary_expansion'_0or1[of r] by blast have "r = (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (âi::nat. real (r01_binary_expansion' r (i + (Suc n))) * ((1/2)^(Suc (i + (Suc n)))))" proof - have "r = (âl. real (r01_binary_expansion' r l) * (1 / 2) ^ Suc l)" using r01_binary_expression_correct[of r] assms by simp also have "... = (âl. real (r01_binary_expansion' r (l + Suc n)) * (1 / 2) ^ Suc (l + Suc n)) + (âi<Suc n. real (r01_binary_expansion' r i) * (1 / 2) ^ Suc i)" apply(rule suminf_split_initial_segment) apply(rule binary_expression_summable) using real01_binary_expansion'_0or1[of r] by simp also have "... = (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (âi::nat. real (r01_binary_expansion' r (i + (Suc n))) * ((1/2)^(Suc (i + (Suc n)))))" proof - have "ân. {..<Suc n} = {0..n}" by auto thus ?thesis by simp qed finally show ?thesis . qed also have "... = (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (âi::nat. ((1/2)^(Suc (i + (Suc n)))))" using h by simp also have "... = (âi=0..n. real (r01_binary_expansion' r i) * ((1/2)^(Suc i))) + (1/2)^(Suc n)" using half_sum[of "Suc n"] by simp also have "... = lr + (1/2)^(Suc n)" using 1 r01_binary_expression_eq_lr[of r n] by(simp add: r01_binary_expression_def r01_binary_sum_def) also have "... = ur" using r01_binary_expansion_diff[of r n] by(simp add: 1) finally have "r = ur" . moreover have "r < ur" using r01_binary_expansion_lr_r_ur[of r n] assms 1 by simp ultimately show False by simp qed qed text â¹ A binary expression is well-formed when $111\dots$ does not appear in the tail of the sequence ⺠definition biexp01_well_formed :: "(nat â nat) â bool" where "biexp01_well_formed a â¡ (ân. a n â {0,1}) â§ (ân. âmâ¥n. a m = 0)" lemma biexp01_well_formedE: assumes "biexp01_well_formed a" shows "(ân. a n â {0,1}) â§ (ân. âmâ¥n. a m = 0)" using assms by(simp add: biexp01_well_formed_def) lemma biexp01_well_formedI: assumes "ân. a n â {0,1}" and "ân. âmâ¥n. a m = 0" shows "biexp01_well_formed a" using assms by(simp add: biexp01_well_formed_def) lemma r01_binary_expansion_well_formed: assumes "0 < r" "r < 1" shows "biexp01_well_formed (r01_binary_expansion' r)" using r01_binary_expression_ex0_strong[of r] assms real01_binary_expansion'_0or1[of r] by(simp add: biexp01_well_formed_def) lemma biexp01_well_formed_comb: assumes "biexp01_well_formed a" and "biexp01_well_formed b" shows "biexp01_well_formed (λn. if even n then a (n div 2) else b ((n-1) div 2))" proof(rule biexp01_well_formedI) show "ân. (if even n then a (n div 2) else b ((n - 1) div 2)) â {0, 1}" using assms biexp01_well_formedE by simp next fix n obtain m where 1:"mâ¥n â§ a m = 0" using assms biexp01_well_formedE by blast then have "a ((2*m) div 2) = 0" by simp hence "(if even (2*m) then a (2*m div 2) else b ((2*m - 1) div 2)) = 0" by simp moreover have "2*m ⥠n" using 1 by simp ultimately show "âmâ¥n. (if even m then a (m div 2) else b ((m - 1) div 2)) = 0" by auto qed lemma nat_complete_induction: assumes "P (0 :: nat)" and "ân. (âm. m ⤠n â¹ P m) â¹ P (Suc n)" shows "P n" proof(cases n) case 0 then show ?thesis using assms(1) by simp next case h:(Suc n') have "P (Suc n')" proof(rule assms(2)) show "âm. m ⤠n' â¹ P m" proof(induction n') case 0 then show ?case using assms(1) by simp next case (Suc n'') then show ?case by (metis assms(2) le_SucE) qed qed thus ?thesis using h by simp qed text â¹ â¹(âm. real (a m) * (1 / 2) ^ Suc m) n = a nâº.⺠lemma biexp01_well_formed_an: assumes "biexp01_well_formed a" shows "r01_binary_expansion' (âm. real (a m) * (1 / 2) ^ Suc m) n = a n" proof(rule nat_complete_induction[of _ n]) show "r01_binary_expansion' (âm. real (a m) * (1 / 2) ^ Suc m) 0 = a 0" proof (auto simp add: r01_binary_expansion'_def) assume h:"1 ⤠(âm. real (a m) * (1 / 2) ^ m / 2) * 2" show "Suc 0 = a 0" proof(rule ccontr) assume "Suc 0 â a 0" then have "a 0 = 0" using assms(1) biexp01_well_formedE[of a] by auto hence "(âm. real (a m) * (1 / 2) ^ (Suc m)) = (âm. real (a (Suc m)) * (1 / 2) ^ (Suc (Suc m)))" using suminf_split_head[of "λm. real (a m) * (1 / 2) ^ (Suc m)"] binary_expression_summable[of a] assms biexp01_well_formedE by simp also have "... < 1/2" using ai_exists0_less_than_sum[of a 1] assms biexp01_well_formedE[of a] by auto finally have "(âm. real (a m) * (1 / 2) ^ m / 2) < 1/2" by simp thus False using h by simp qed next assume h:"¬ 1 ⤠(âm. real (a m) * (1 / 2) ^ m / 2) * 2" show "a 0 = 0" proof(rule ccontr) assume "a 0 â 0" then have "a 0 = 1" using assms(1) biexp01_well_formedE[of a] by (meson insertE singletonD) hence "1/2 ⤠(âm. real (a m) * (1 / 2) ^ (Suc m))" using ai_1_gt[of a 0] assms(1) biexp01_well_formedE[of a] by auto thus False using h by simp qed qed next fix n :: nat assume ih:"(âm. m ⤠n â¹ r01_binary_expansion' (âm. real (a m) * (1 / 2) ^ Suc m) m = a m)" show "r01_binary_expansion' (âm. real (a m) * (1 / 2) ^ Suc m) (Suc n) = a (Suc n)" proof(cases "r01_binary_expansion'' (âm. real (a m) * (1 / 2) ^ Suc m) n") case h:(fields bn ur lr) then have hlr:"lr = (âk=0..n. real (a k) * (1 / 2) ^ Suc k)" using r01_binary_expression_eq_lr[of "âm. real (a m) * (1 / 2) ^ Suc m" n] ih by(simp add: r01_binary_expression_def r01_binary_sum_def) have hlr2:"(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n))" proof - have "(ur + lr) / 2 = lr + (1/2)^(Suc (Suc n))" using r01_binary_expansion_diff[of "âm. real (a m) * (1 / 2) ^ Suc m" n] h by simp show ?thesis by (simp add: â¹(ur + lr) / 2 = lr + (1 / 2) ^ Suc (Suc n)⺠of_rat_add of_rat_divide of_rat_power) qed show ?thesis using h proof(auto simp add: r01_binary_expansion'_def Let_def) assume h1: "(ur + lr) ⤠(âm. real (a m) * (1 / 2) ^ m / 2) * 2" show "Suc 0 = a (Suc n)" proof(rule ccontr) assume "Suc 0 â a (Suc n)" then have "a (Suc n) = 0" using assms(1) biexp01_well_formedE[of a] by auto have "(âm. real (a m) * (1 / 2) ^ m / 2) < (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^(Suc (Suc n))" proof - have "(âm. real (a m) * (1 / 2) ^ (Suc m)) = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (m+Suc n)) * (1 / 2) ^ Suc (m + Suc n))" proof - have "{0..n} = {..<Suc n}" by auto thus ?thesis using suminf_split_initial_segment[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a] by simp qed also have "... = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (Suc m + Suc n)) * (1 / 2) ^ Suc (Suc m + Suc n))" using suminf_split_head[of "λm. real (a (m + Suc n)) * (1 / 2) ^ (Suc (m + Suc n))"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a] Series.summable_iff_shift[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] â¹a (Suc n) = 0⺠by simp also have "... = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (m + Suc (Suc n))) * (1 / 2) ^ Suc (m + Suc (Suc n)))" by simp also have "... < (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^Suc (Suc n)" using ai_exists0_less_than_sum[of a "Suc (Suc n)"] assms(1) biexp01_well_formedE[of a] by auto finally show ?thesis by simp qed thus False using h1 hlr2 hlr by simp qed next assume h2:"¬ ur + lr ⤠(âm. real (a m) * (1 / 2) ^ m / 2) * 2" show "a (Suc n) = 0" proof(rule ccontr) assume "a (Suc n) â 0" then have "a (Suc n) = 1" using biexp01_well_formedE[OF assms(1)] by (meson insertE singletonD) have "(âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (1/2)^(Suc (Suc n)) ⤠(âm. real (a m) * (1 / 2) ^ m / 2)" proof - have "(âm. real (a m) * (1 / 2) ^ (Suc m)) = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (m+Suc n)) * (1 / 2) ^ Suc (m + Suc n))" proof - have "{0..n} = {..<Suc n}" by auto thus ?thesis using suminf_split_initial_segment[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a] by simp qed also have "... = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (Suc m + Suc n)) * (1 / 2) ^ Suc (Suc m + Suc n)) + (1 / 2) ^ Suc (Suc n)" using suminf_split_head[of "λm. real (a (m + Suc n)) * (1 / 2) ^ (Suc (m + Suc n))"] binary_expression_summable[of a] assms(1) biexp01_well_formedE[of a] Series.summable_iff_shift[of "λm. real (a m) * (1 / 2) ^ (Suc m)" "Suc n"] â¹a (Suc n) = 1⺠by simp also have "... = (âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (âm. real (a (m + Suc (Suc n))) * (1 / 2) ^ Suc (m + (Suc (Suc n)))) + (1 / 2) ^ Suc (Suc n)" by simp also have "... ⥠(âk=0..n. real (a k) * (1 / 2) ^ Suc k) + (1 / 2) ^ Suc (Suc n)" using binary_expression_gteq0[of a "Suc (Suc n)"] assms(1) biexp01_well_formedE[of a] by simp finally show ?thesis by simp qed thus False using h2 hlr2 hlr by simp qed qed qed qed lemma f01_borel_measurable: assumes "f -` {0::real} â sets real_borel" "f -` {1} â sets borel" and "âr::real. f r â {0,1}" shows "f â borel_measurable real_borel" proof(rule measurableI) fix U :: "real set" assume "U â sets borel" consider "1 â U â§ 0 â U" | "1 â U â§ 0 â U" | "1 â U â§ 0 â U" | "1 â U â§ 0 â U" by auto then show "f -` U â© space real_borel â sets borel" proof cases case 1 then have "f -` U = UNIV" using assms(3) by auto then show ?thesis by simp next case 2 then have "f -` U = f -` {1}" using assms(3) by fastforce then show ?thesis using assms(2) by simp next case 3 then have "f -` U = f -` {0}" using assms(3) by fastforce then show ?thesis using assms(1) by simp next case 4 then have "f -` U = {}" using assms(3) by (metis all_not_in_conv insert_iff vimage_eq) then show ?thesis by simp qed qed simp lemma r01_binary_expansion'_measurable: "(λr. real (r01_binary_expansion' r n)) â borel_measurable (borel :: real measure)" proof - have "(λr. real (r01_binary_expansion' r n)) -`{0} â sets borel â§ (λr. real (r01_binary_expansion' r n)) -`{1} â sets borel" proof - let ?A = "{..0::real} ⪠(âiâ{l::nat. l < 2^(Suc n) â§ even l} . {i/2^(Suc n)..<(Suc i)/2^(Suc n)})" let ?B = "{1::real..} ⪠(âiâ{l::nat. l < 2^(Suc n) â§ odd l} . {i/2^(Suc n)..<(Suc i)/2^(Suc n)})" have "?A â sets borel" by simp have "?B â sets borel" by simp have hE:"?A â© ?B = {}" proof auto fix r :: real fix l :: nat assume h: "r ⤠0" "odd l" "real l / (2 * 2 ^ n) ⤠r" then have "0 < l" by(cases l; auto) hence "0 < real l / (2 * 2 ^ n)" by simp thus False using h by simp next fix r :: real fix l :: nat assume h: "l < 2 * 2 ^ n" "even l" "1 ⤠r" "r < (1 + real l) / (2 * 2 ^ n)" then have "1 + real l ⤠2 * 2 ^ n" by (simp add: nat_less_real_le) moreover have "1 + real l â 2 * 2 ^ n" using h by auto ultimately have "1 + real l < 2 * 2 ^ n" by simp hence "(1 + real l) / (2 * 2 ^ n) < 1" by simp thus False using h by linarith next fix r :: real fix l1 l2 :: nat assume h: "even l1" "odd l2" "real l1 / (2 * 2 ^ n) ⤠r" "r < (1 + real l1) / (2 * 2 ^ n)" "real l2 / (2 * 2 ^ n) ⤠r" "r < (1 + real l2) / (2 * 2 ^ n)" then consider "l1 < l2" | "l2 < l1" by fastforce thus False proof cases case 1 then have "(1 + real l1) / (2 * 2 ^ n) ⤠real l2 / (2 * 2 ^ n)" by (simp add: frac_le) then show ?thesis using h by simp next case 2 then have "(1 + real l2) / (2 * 2 ^ n) ⤠real l1 / (2 * 2 ^ n)" by (simp add: frac_le) then show ?thesis using h by simp qed qed have hU:"?A ⪠?B = UNIV" proof show "?A ⪠?B â UNIV" by simp next show "UNIV â ?A ⪠?B" proof fix r :: real consider "r ⤠0" | "0 < r â§ r < 1" | "1 ⤠r" by linarith then show "r â ?A ⪠?B" proof cases case 1 then show ?thesis by simp next case 2 show ?thesis proof(cases "r01_binary_expansion'' r n") case hc:(fields a ur lr) then have hlu:"lr ⤠r â§ r < ur" using 2 r01_binary_expansion_lr_r_ur[of r n] by simp obtain k :: nat where hk: "lr = real k / 2 ^ Suc n â§ k < 2 ^ Suc n" using r01_binary_expression'_sum_range[of r n] hc by auto hence "ur = real (Suc k) / 2^Suc n" using r01_binary_expansion_diff[of r n] hc by (simp add: add_divide_distrib power_one_over) thus ?thesis using hlu hk by auto qed next case 3 then show ?thesis by simp qed qed qed have hi1:"- ?A = ?B" proof - have "?B â - ?A" using hE by blast moreover have "-?A â ?B" proof - have "-(?A ⪠?B) = {}" using hU by simp hence "(-?A) â© (-?B) = {}" by simp thus ?thesis by blast qed ultimately show ?thesis by blast qed have hi2: "?A = -?B" using hi1 by blast let ?U0 = "(λr. real (r01_binary_expansion' r n)) -`{0}" let ?U1 = "(λr. real (r01_binary_expansion' r n)) -`{1}" have hU':"?U0 ⪠?U1 = UNIV" proof - have "?U0 ⪠?U1 = (λr. real (r01_binary_expansion' r n)) -`{0,1}" by auto thus ?thesis using real01_binary_expansion'_0or1[of _ n] by auto qed have hE':"?U0 â© ?U1 = {}" by auto have hiu1:"- ?U0 = ?U1" using hE' hU' by fastforce have hiu2:"- ?U1 = ?U0" using hE' hU' by fastforce have "?U0 â ?A" proof fix r assume "r â ?U0" then have h1:"r01_binary_expansion' r n = 0" by simp then consider "r ⤠0" | "0 < r â§ r < 1" using r01_binary_expansion'_gt1[of r] by fastforce thus "r â ?A" proof cases case 1 then show ?thesis by simp next case 2 then have 3:"(snd (snd (r01_binary_expansion'' r n))) ⤠r â§ r < (fst (snd (r01_binary_expansion'' r n)))" using r01_binary_expansion_lr_r_ur[of r n] by simp obtain k where 4: "(snd (snd (r01_binary_expansion'' r n))) = real k / 2 ^ Suc n â§ k < 2 ^ Suc n â§ even k" using r01_binary_expression'_sum_range[of r n] h1 by auto have "(fst (snd (r01_binary_expansion'' r n))) = real (Suc k) / 2 ^ Suc n" proof - have "(fst (snd (r01_binary_expansion'' r n))) = (snd (snd (r01_binary_expansion'' r n))) + (1/2)^Suc n" using r01_binary_expansion_diff[of r n] by linarith thus ?thesis using 4 by (simp add: add_divide_distrib power_one_over) qed thus ?thesis using 3 4 by auto qed qed have "?U1 â ?B" proof fix r assume "r â ?U1" then have h1:"r01_binary_expansion' r n = 1" by simp then consider "1 ⤠r" | "0 < r â§ r < 1" using r01_binary_expansion'_lt0[of r] by fastforce thus "r â ?B" proof cases case 1 then show ?thesis by simp next case 2 then have 3:"(snd (snd (r01_binary_expansion'' r n))) ⤠r â§ r < (fst (snd (r01_binary_expansion'' r n)))" using r01_binary_expansion_lr_r_ur[of r n] by simp obtain k where 4: "(snd (snd (r01_binary_expansion'' r n))) = real k / 2 ^ Suc n â§ k < 2 ^ Suc n â§ odd k" using StandardBorel.r01_binary_expression'_sum_range[of r n] h1 by auto have "(fst (snd (r01_binary_expansion'' r n))) = real (Suc k) / 2 ^ Suc n" proof - have "(fst (snd (r01_binary_expansion'' r n))) = (snd (snd (r01_binary_expansion'' r n))) + (1/2)^Suc n" using r01_binary_expansion_diff[of r n] by simp thus ?thesis using 4 by (simp add: add_divide_distrib power_one_over) qed thus ?thesis using 3 4 by auto qed qed have "?U0 = ?A" proof show "?U0 â ?A" by fact next show "?A â ?U0" using â¹?U1 â ?B⺠Compl_subset_Compl_iff[of ?U0 ?A] hi1 hiu1 by blast qed have "?U1 = ?B" using â¹?U0 = ?A⺠hi1 hiu1 by auto show ?thesis using â¹?U0 = ?A⺠â¹?U1 = ?B⺠â¹?A â sets borel⺠â¹?B â sets borel⺠by simp qed thus ?thesis using f01_borel_measurable[of "(λr. real (r01_binary_expansion' r n))"] real01_binary_expansion'_0or1[of _ n] by simp qed (* (0,1) â [0,1]Ã[0,1]. *) definition r01_to_r01_r01_fst' :: "real â nat â nat" where "r01_to_r01_r01_fst' r n â¡ r01_binary_expansion' r (2*n)" lemma r01_to_r01_r01_fst'in01: "ân. r01_to_r01_r01_fst' r n â {0,1}" using real01_binary_expansion'_0or1 by (simp add: r01_to_r01_r01_fst'_def) definition r01_to_r01_r01_fst_sum :: "real â nat â real" where "r01_to_r01_r01_fst_sum â¡ r01_binary_sum â r01_to_r01_r01_fst'" definition r01_to_r01_r01_fst :: "real â real" where "r01_to_r01_r01_fst = lim â r01_to_r01_r01_fst_sum" lemma r01_to_r01_r01_fst_def': "r01_to_r01_r01_fst r = (ân. real (r01_binary_expansion' r (2*n)) * (1/2)^(n+1))" proof - have "r01_to_r01_r01_fst_sum r = (λn. âi=0..n. real (r01_binary_expansion' r (2*i)) * (1/2)^(i+1))" by(auto simp add: r01_to_r01_r01_fst_sum_def r01_binary_sum_def r01_to_r01_r01_fst'_def) thus ?thesis using lim_sum_ai real01_binary_expansion'_0or1 by(simp add: r01_to_r01_r01_fst_def) qed lemma r01_to_r01_r01_fst_measurable: "r01_to_r01_r01_fst â borel_measurable borel" unfolding r01_to_r01_r01_fst_def' using r01_binary_expansion'_measurable by auto definition r01_to_r01_r01_snd' :: "real â nat â nat" where "r01_to_r01_r01_snd' r n = r01_binary_expansion' r (2*n + 1)" lemma r01_to_r01_r01_snd'in01: "ân. r01_to_r01_r01_snd' r n â {0,1}" using real01_binary_expansion'_0or1 by (simp add: r01_to_r01_r01_snd'_def) definition r01_to_r01_r01_snd_sum :: "real â nat â real" where "r01_to_r01_r01_snd_sum â¡ r01_binary_sum â r01_to_r01_r01_snd'" definition r01_to_r01_r01_snd :: "real â real" where "r01_to_r01_r01_snd = lim â r01_to_r01_r01_snd_sum" lemma r01_to_r01_r01_snd_def': "r01_to_r01_r01_snd r = (ân. real (r01_binary_expansion' r (2*n + 1)) * (1/2)^(n+1))" proof - have "r01_to_r01_r01_snd_sum r = (λn. âi=0..n. real (r01_binary_expansion' r (2*i + 1)) * (1/2)^(i+1))" by(auto simp add: r01_to_r01_r01_snd_sum_def r01_binary_sum_def r01_to_r01_r01_snd'_def) thus ?thesis using lim_sum_ai real01_binary_expansion'_0or1 by(simp add: r01_to_r01_r01_snd_def) qed lemma r01_to_r01_r01_snd_measurable: "r01_to_r01_r01_snd â borel_measurable borel" unfolding r01_to_r01_r01_snd_def' using r01_binary_expansion'_measurable by auto definition r01_to_r01_r01 :: "real â real à real" where "r01_to_r01_r01 r = (r01_to_r01_r01_fst r,r01_to_r01_r01_snd r)" lemma r01_to_r01_r01_image: "r01_to_r01_r01 r â {0..1}Ã{0..1}" using r01_to_r01_r01_fst_def'[of r] r01_to_r01_r01_snd_def'[of r] real01_binary_expansion'_0or1 binary_expression_gteq0[of "λn. r01_binary_expansion' r (2*n)" 0] binary_expression_leeq1[of "λn. r01_binary_expansion' r (2*n)" 0] binary_expression_gteq0[of "λn. r01_binary_expansion' r (2*n+1)" 0] binary_expression_leeq1[of "λn. r01_binary_expansion' r (2*n+1)" 0] by(simp add: r01_to_r01_r01_def) lemma r01_to_r01_r01_measurable: "r01_to_r01_r01 â real_borel ââ©M real_borel â¨â©M real_borel" unfolding r01_to_r01_r01_def using borel_measurable_Pair[of r01_to_r01_r01_fst borel r01_to_r01_r01_snd] r01_to_r01_r01_fst_measurable r01_to_r01_r01_snd_measurable by(simp add: borel_prod) lemma r01_to_r01_r01_3over4: "r01_to_r01_r01 (3/4) = (1/2,1/2)" proof - have h0:"r01_binary_expansion' (3/4) 0 = 1" by (simp add: r01_binary_expansion'_def) have h1:"r01_binary_expansion' (3/4) 1 = 1" by (simp add: r01_binary_expansion'_def Let_def of_rat_divide) have hn:"ân. n>1â¹ r01_binary_expansion' (3/4) n = 0" proof - fix n :: nat assume h:"1 < n" show "r01_binary_expansion' (3 / 4) n = 0" proof(rule ccontr) assume "r01_binary_expansion' (3 / 4) n â 0" have "3/4 < (âi=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))" proof - have "(âi=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) = real (r01_binary_expansion' (3/4) 0) * (1/2)^(Suc 0) + (âi=(Suc 0)..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))" by(rule sum.atLeast_Suc_atMost) (simp add: h) also have "... = real (r01_binary_expansion' (3/4) 0) * (1/2)^(Suc 0) + (real (r01_binary_expansion' (3/4) 1) * (1/2)^(Suc 1) + (âi=(Suc (Suc 0))..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)))" using sum.atLeast_Suc_atMost[OF order.strict_implies_order[OF h],of "λi. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)"] by simp also have "... = 3/4 + (âi=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))" using h0 h1 by(simp add: numeral_2_eq_2) also have "... > 3/4" proof - have "(âi=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) = (âi=2..n-1. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) + real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n" by (metis (no_types, lifting) h One_nat_def Suc_pred less_2_cases_iff less_imp_add_positive order_less_irrefl plus_1_eq_Suc sum.cl_ivl_Suc zero_less_Suc) hence "real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n ⤠(âi=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))" using ordered_comm_monoid_add_class.sum_nonneg[of "{2..n-1}" "λi. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)"] by simp moreover have "0 < real (r01_binary_expansion' (3/4) n) * (1/2)^Suc n" using â¹r01_binary_expansion' (3 / 4) n â 0⺠by simp ultimately have "0 < (âi=2..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i))" by simp thus ?thesis by simp qed finally show "3 / 4 < (âi = 0..n. real (r01_binary_expansion' (3 / 4) i) * (1 / 2) ^ Suc i)" . qed moreover have "(âi=0..n. real (r01_binary_expansion' (3/4) i) * (1/2)^(Suc i)) ⤠3/4" using r01_binary_expansion_lr_r_ur[of "3/4" n] r01_binary_expression_eq_lr[of "3/4" n] by(simp add: r01_binary_expression_def r01_binary_sum_def) ultimately show False by simp qed qed show ?thesis proof have "fst (r01_to_r01_r01 (3 / 4)) = (ân. real (r01_binary_expansion' (3 / 4) (2 * n)) * (1 / 2) ^ Suc n)" by(simp add: r01_to_r01_r01_def r01_to_r01_r01_fst_def') also have "... = 1/2 + (ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n))" using suminf_split_head[of "λn. real (r01_binary_expansion' (3 / 4) (2 * n)) * (1 / 2) ^ Suc n"] binary_expression_summable[of "λn. r01_binary_expansion' (3/4) (2*n)"] real01_binary_expansion'_0or1[of "3/4"] h0 by simp also have "... = 1/2" proof - have "ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n) = 0" using hn by simp hence "(ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n)) * (1 / 2) ^ Suc (Suc n)) = 0" by simp thus ?thesis by simp qed finally show "fst (r01_to_r01_r01 (3 / 4)) = fst (1 / 2, 1 / 2)" by simp next have "snd (r01_to_r01_r01 (3 / 4)) = (ân. real (r01_binary_expansion' (3 / 4) (2 * n + 1)) * (1 / 2) ^ Suc n)" by(simp add: r01_to_r01_r01_def r01_to_r01_r01_snd_def') also have "... = 1/2 + (ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n))" using suminf_split_head[of "λn. real (r01_binary_expansion' (3 / 4) (2 * n + 1)) * (1 / 2) ^ Suc n"] binary_expression_summable[of "λn. r01_binary_expansion' (3/4) (2*n + 1)"] real01_binary_expansion'_0or1[of "3/4"] h1 by simp also have "... = 1/2" proof - have "ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n) = 0" using hn by simp hence "(ân. real (r01_binary_expansion' (3 / 4) (2 * Suc n + 1)) * (1 / 2) ^ Suc (Suc n)) = 0" by simp thus ?thesis by simp qed finally show "snd (r01_to_r01_r01 (3 / 4)) = snd (1 / 2, 1 / 2)" by simp qed qed (* (0,1)Ã(0,1) â (0,1). *) definition r01_r01_to_r01' :: "real à real â nat â nat" where "r01_r01_to_r01' rs â¡ (λn. if even n then r01_binary_expansion' (fst rs) (n div 2) else r01_binary_expansion' (snd rs) ((n-1) div 2))" lemma r01_r01_to_r01'in01: "ân. r01_r01_to_r01' rs n â {0,1}" using real01_binary_expansion'_0or1 by (simp add: r01_r01_to_r01'_def) lemma r01_r01_to_r01'_well_formed: assumes "0 < r1" "r1 < 1" and "0 < r2" "r2 < 1" shows "biexp01_well_formed (r01_r01_to_r01' (r1,r2))" using biexp01_well_formed_comb[of "r01_binary_expansion' (fst (r1,r2))" "r01_binary_expansion' (snd (r1,r2))"] r01_binary_expansion_well_formed[of r1] r01_binary_expansion_well_formed[of r2] assms by (auto simp add: r01_r01_to_r01'_def) definition r01_r01_to_r01_sum :: "real à real â nat â real" where "r01_r01_to_r01_sum â¡ r01_binary_sum â r01_r01_to_r01'" definition r01_r01_to_r01 :: "real à real â real" where "r01_r01_to_r01 â¡ lim â r01_r01_to_r01_sum" lemma r01_r01_to_r01_def': "r01_r01_to_r01 (r1,r2) = (ân. real (r01_r01_to_r01' (r1,r2) n) * (1/2)^(n+1))" proof - have "r01_r01_to_r01_sum (r1,r2) = (λn. (âi = 0..n. real (r01_r01_to_r01' (r1,r2) i) * (1 / 2) ^ Suc i))" by(auto simp add: r01_r01_to_r01_sum_def r01_binary_sum_def) thus ?thesis using lim_sum_ai[of "λn. r01_r01_to_r01' (r1,r2) n"] r01_r01_to_r01'in01 by(simp add: r01_r01_to_r01_def) qed lemma r01_r01_to_r01_measurable: "r01_r01_to_r01 â real_borel â¨â©M real_borel ââ©M real_borel" proof - have "r01_r01_to_r01 = (λx. ân. real (r01_r01_to_r01' x n) * (1/2)^(n+1))" using r01_r01_to_r01_def' by auto also have "... â real_borel â¨â©M real_borel ââ©M real_borel" proof(rule borel_measurable_suminf) fix n :: nat have "(λx. real (r01_r01_to_r01' x n) * (1 / 2) ^ (n + 1)) = (λr. r * (1/2)^(n+1)) â (λx. real (r01_r01_to_r01' x n))" by auto also have "... â borel_measurable (borel â¨â©M borel)" proof(rule measurable_comp[of _ _ borel]) have "(λx. real (r01_r01_to_r01' x n)) = (λx. if even n then real (r01_binary_expansion' (fst x) (n div 2)) else real (r01_binary_expansion' (snd x) ((n - 1) div 2)))" by (auto simp add: r01_r01_to_r01'_def) also have "... â borel_measurable (borel â¨â©M borel)" using r01_binary_expansion'_measurable by simp finally show "(λx. real (r01_r01_to_r01' x n)) â borel_measurable (borel â¨â©M borel)" . next show "(λr::real. r * (1 / 2) ^ (n + 1)) â borel_measurable borel" by simp qed finally show "(λx. real (r01_r01_to_r01' x n) * (1 / 2) ^ (n + 1)) â borel_measurable (borel â¨â©M borel)" . qed finally show ?thesis . qed lemma r01_r01_to_r01_image: assumes "0 < r1" "r1 < 1" shows "r01_r01_to_r01 (r1,r2) â {0<..<1}" proof - obtain i where "r01_binary_expansion' r1 i = 1" using r01_binary_expression_ex1[of r1] assms(1,2) by auto hence hi:"r01_r01_to_r01' (r1,r2) (2*i) = 1" by(simp add: r01_r01_to_r01'_def) obtain j where "r01_binary_expansion' r1 j = 0" using r01_binary_expression_ex0[of r1] assms(1,2) by auto hence hj:"r01_r01_to_r01' (r1,r2) (2*j) = 0" by(simp add: r01_r01_to_r01'_def) show ?thesis using ai_exists1_gt0[of "r01_r01_to_r01' (r1,r2)"] ai_exists0_less_than1[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'in01[of "(r1,r2)"] r01_r01_to_r01_def'[of r1 r2] hi hj by auto qed lemma r01_r01_to_r01_image': assumes "0 < r2" "r2 < 1" shows "r01_r01_to_r01 (r1,r2) â {0<..<1}" proof - obtain i where "r01_binary_expansion' r2 i = 1" using r01_binary_expression_ex1[of r2] assms(1,2) by auto hence hi:"r01_r01_to_r01' (r1,r2) (2*i + 1) = 1" by(simp add: r01_r01_to_r01'_def) obtain j where "r01_binary_expansion' r2 j = 0" using r01_binary_expression_ex0[of r2] assms(1,2) by auto hence hj:"r01_r01_to_r01' (r1,r2) (2*j + 1) = 0" by(simp add: r01_r01_to_r01'_def) show ?thesis using ai_exists1_gt0[of "r01_r01_to_r01' (r1,r2)"] ai_exists0_less_than1[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'in01[of "(r1,r2)"] r01_r01_to_r01_def'[of r1 r2] hi hj by auto qed lemma r01_r01_to_r01_binary_nth: assumes "0 < r1" "r1 < 1" and "0 < r2" "r2 < 1" shows "r01_binary_expansion' r1 n = r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) (2*n) â§ r01_binary_expansion' r2 n = r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) (2*n + 1)" proof - have "ân. r01_binary_expansion' (r01_r01_to_r01 (r1,r2)) n = r01_r01_to_r01' (r1,r2) n" using r01_r01_to_r01_def'[of r1 r2] biexp01_well_formed_an[of "r01_r01_to_r01' (r1,r2)"] r01_r01_to_r01'_well_formed[of r1 r2] assms by simp thus ?thesis by(simp add: r01_r01_to_r01'_def) qed lemma r01_r01__r01__r01_r01_id: assumes "0 < r1" "r1 < 1" "0 < r2" "r2 < 1" shows "(r01_to_r01_r01 â r01_r01_to_r01) (r1,r2) = (r1,r2)" proof show "fst ((r01_to_r01_r01 â r01_r01_to_r01) (r1, r2)) = fst (r1, r2)" proof - have "fst ((r01_to_r01_r01 â r01_r01_to_r01) (r1, r2)) = r01_to_r01_r01_fst (r01_r01_to_r01 (r1,r2))" by(simp add: r01_to_r01_r01_def) also have "... = (ân. real (r01_binary_expansion' (r01_r01_to_r01 (r1, r2)) (2 * n)) * (1 / 2) ^ (n + 1))" using r01_to_r01_r01_fst_def'[of "r01_r01_to_r01 (r1,r2)"] by simp also have "... = (ân. real (r01_binary_expansion' r1 n) * (1 / 2) ^ (n + 1))" using r01_r01_to_r01_binary_nth[of r1 r2] assms by simp also have "... = r1" using r01_binary_expression_correct[of r1] assms(1,2) by simp finally show ?thesis by simp qed next show "snd ((r01_to_r01_r01 â r01_r01_to_r01) (r1, r2)) = snd (r1, r2)" proof - have "snd ((r01_to_r01_r01 â r01_r01_to_r01) (r1, r2)) = r01_to_r01_r01_snd (r01_r01_to_r01 (r1,r2))" by(simp add: r01_to_r01_r01_def) also have "... = (ân. real (r01_binary_expansion' (r01_r01_to_r01 (r1, r2)) (2 * n + 1)) * (1 / 2) ^ (n + 1))" using r01_to_r01_r01_snd_def'[of "r01_r01_to_r01 (r1,r2)"] by simp also have "... = (ân. real (r01_binary_expansion' r2 n) * (1 / 2) ^ (n + 1))" using r01_r01_to_r01_binary_nth[of r1 r2] assms by simp also have "... = r2" using r01_binary_expression_correct[of r2] assms(3,4) by simp finally show ?thesis by simp qed qed text â¹ We first show that â¹M â¨â©M N⺠is a standard Borel space for standard Borel spaces â¹M⺠and â¹Nâº.⺠lemma pair_measurable[measurable]: assumes "f â X ââ©M Y" and "g â X' ââ©M Y'" shows "map_prod f g â X â¨â©M X' ââ©M Y â¨â©M Y'" using assms by(auto simp add: measurable_pair_iff) lemma pair_standard_borel_standard: assumes "standard_borel M" and "standard_borel N" shows "standard_borel (M â¨â©M N)" proof - â â¹ First, define the measurable function $\mathbb{R} \times \mathbb{R} \rightarrow \mathbb{R}$.⺠define rr_to_r :: "real à real â real" where "rr_to_r â¡ real_to_01open_inverse â r01_r01_to_r01 â (λ(x,y). (real_to_01open x, real_to_01open y))" â â¹ $\mathbb{R}\times\mathbb{R} \rightarrow (0,1)\times(0,1) \rightarrow (0,1) \rightarrow \mathbb{R}$.⺠have 1[measurable]: "rr_to_r â real_borel â¨â©M real_borel ââ©M real_borel" proof - have "(λ(x,y). (real_to_01open x, real_to_01open y)) â real_borel â¨â©M real_borel ââ©M real_borel â¨â©M real_borel" using borel_measurable_continuous_onI[OF real_to_01open_continuous] by simp from measurable_restrict_space2[OF _ this,of "{0<..<1}Ã{0<..<1}"] have [measurable]:"(λ(x,y). (real_to_01open x, real_to_01open y)) â real_borel â¨â©M real_borel ââ©M restrict_space (real_borel â¨â©M real_borel) ({0<..<1}Ã{0<..<1})" by(simp add: split_beta' real_to_01open_01) have [measurable]: "r01_r01_to_r01 â restrict_space (real_borel â¨â©M real_borel) ({0<..<1}Ã{0<..<1}) ââ©M restrict_space real_borel {0<..<1}" using r01_r01_to_r01_image' by(auto intro!: measurable_restrict_space3[OF r01_r01_to_r01_measurable]) thus ?thesis using borel_measurable_continuous_on_restrict[OF real_to_01open_inverse_continuous] by(simp add: rr_to_r_def) qed â â¹ Next, define the measurable function $\mathbb{R}\rightarrow \mathbb{R}\times\mathbb{R}$.⺠define r_to_01 :: "real â real" where "r_to_01 â¡ (λr. if r â real_to_01open -` (r01_to_r01_r01 -` ({0<..<1}Ã{0<..<1})) then real_to_01open r else 3/4)" define r01_to_r01_r01' :: "real â real à real" where "r01_to_r01_r01' â¡ (λr. if r â r01_to_r01_r01 -` ({0<..<1}Ã{0<..<1}) then r01_to_r01_r01 r else (1/2,1/2))" define r_to_rr :: "real â real à real" where "r_to_rr â¡ (λ(x,y). (real_to_01open_inverse x, real_to_01open_inverse y)) â r01_to_r01_r01' â r_to_01" â â¹ $\mathbb{R} \rightarrow (0,1) \rightarrow (0,1)\times(0,1) \rightarrow \mathbb{R}\times\mathbb{R}$.⺠have 2[measurable]: "r_to_rr â real_borel ââ©M real_borel â¨â©M real_borel" proof - have 1: "{0<..<1}Ã{0<..<1} â sets (restrict_space (real_borel â¨â©M real_borel) ({0..1}Ã{0..1}))" by(auto simp: sets_restrict_space_iff) have 2[measurable]: "real_to_01open â real_borel ââ©M restrict_space real_borel {0<..<1}" using measurable_restrict_space2[OF _ borel_measurable_continuous_onI[OF real_to_01open_continuous] ,of "{0<..<1}"] by(simp add: real_to_01open_01) have 3: "real_to_01open -` space (restrict_space real_borel {0<..<1}) = UNIV" using real_to_01open_01 by auto have "r01_to_r01_r01 â restrict_space real_borel {0<..<1} ââ©M restrict_space (real_borel â¨â©M real_borel) ({0..1}Ã{0..1})" using r01_to_r01_r01_image measurable_restrict_space3[OF r01_to_r01_r01_measurable] by simp note 4 = measurable_sets[OF this 1] note 5 = measurable_sets[OF 2 4,simplified vimage_Int 3,simplified] have [measurable]:"r_to_01 â real_borel ââ©M restrict_space real_borel {0<..<1}" unfolding r_to_01_def by(rule measurable_If_set) (auto intro!: measurable_restrict_space2 simp: 5) have [measurable]: "r01_to_r01_r01' â restrict_space real_borel {0<..<1} ââ©M restrict_space (real_borel â¨â©M real_borel) ({0<..<1}Ã{0<..<1})" using 4 r01_to_r01_r01_measurable by(auto intro!: measurable_restrict_space3 simp: r01_to_r01_r01'_def) have [measurable]: "(λ(x,y). (real_to_01open_inverse x, real_to_01open_inverse y)) â restrict_space (real_borel â¨â©M real_borel) ({0<..<1}Ã{0<..<1}) ââ©M real_borel â¨â©M real_borel" using borel_measurable_continuous_on_restrict[OF continuous_on_Pair[OF continuous_on_compose[of "{0<..<1::real}Ã{0<..<1::real}",OF continuous_on_fst[OF continuous_on_id'],simplified,OF real_to_01open_inverse_continuous] continuous_on_compose[of "{0<..<1::real}Ã{0<..<1::real}",OF continuous_on_snd[OF continuous_on_id'],simplified,OF real_to_01open_inverse_continuous]]] by(simp add: split_beta' borel_prod) show ?thesis by(simp add: r_to_rr_def) qed have 3: "âx. r_to_rr (rr_to_r x) = x" using r01_to_r01_r01_image r01_r01_to_r01_image r01_r01__r01__r01_r01_id real_to_01open_01 real_to_01open_inverse_correct' fun_cong[OF real_to_01open_inverse_correct] by(auto simp add: r01_to_r01_r01'_def r_to_01_def comp_def split_beta' r_to_rr_def rr_to_r_def) interpret s1: standard_borel M by fact interpret s2: standard_borel N by fact show ?thesis by(auto intro!: standard_borelI[where f="rr_to_r â map_prod s1.f s2.f" and g="map_prod s1.g s2.g â r_to_rr"] simp: 3 space_pair_measure) qed lemma pair_standard_borel_spaceUNIV: assumes "standard_borel_space_UNIV M" and "standard_borel_space_UNIV N" shows "standard_borel_space_UNIV (M â¨â©M N)" apply(rule standard_borel_space_UNIVI') using assms pair_standard_borel_standard[of M N] by(auto simp add: standard_borel_space_UNIV_def standard_borel_space_UNIV_axioms_def space_pair_measure) locale pair_standard_borel = s1: standard_borel M + s2: standard_borel N for M :: "'a measure" and N :: "'b measure" begin sublocale standard_borel "M â¨â©M N" by(auto intro!: pair_standard_borel_standard) end locale pair_standard_borel_space_UNIV = s1: standard_borel_space_UNIV M + s2: standard_borel_space_UNIV N for M :: "'a measure" and N :: "'b measure" begin sublocale pair_standard_borel M N by standard sublocale standard_borel_space_UNIV "M â¨â©M N" by(auto intro!: pair_standard_borel_spaceUNIV simp: s1.standard_borel_space_UNIV_axioms s2.standard_borel_space_UNIV_axioms) end text â¹$\mathbb{R}\times\mathbb{R}$ is a standard Borel space.⺠interpretation real_real : pair_standard_borel_space_UNIV real_borel real_borel by(auto intro!: pair_standard_borel_spaceUNIV simp: real.standard_borel_space_UNIV_axioms pair_standard_borel_space_UNIV_def) subsection â¹ $\mathbb{N}\times\mathbb{R}$ ⺠text â¹ $\mathbb{N}\times\mathbb{R}$ is a standard Borel space. ⺠interpretation nat_real: pair_standard_borel_space_UNIV nat_borel real_borel by(auto intro!: pair_standard_borel_spaceUNIV simp: real.standard_borel_space_UNIV_axioms nat.standard_borel_space_UNIV_axioms pair_standard_borel_space_UNIV_def) end
>
Theory QuasiBorel
(* Title: QuasiBorel.thy Author: Yasuhiko Minamide, Michikazu Hirata, Tokyo Institute of Technology *) section â¹Quasi-Borel Spaces⺠theory QuasiBorel imports "StandardBorel" begin subsection â¹ Definitions ⺠text â¹ We formalize quasi-Borel spaces introduced by Heunen et al.~\cite{Heunen_2017}.⺠subsubsection â¹ Quasi-Borel Spaces⺠definition qbs_closed1 :: "(real â 'a) set â bool" where "qbs_closed1 Mx â¡ (âa â Mx. âf â real_borel ââ©M real_borel. a â f â Mx)" definition qbs_closed2 :: "['a set, (real â 'a) set] â bool" where "qbs_closed2 X Mx â¡ (âx â X. (λr. x) â Mx)" definition qbs_closed3 :: "(real â 'a) set â bool" where "qbs_closed3 Mx â¡ (âP::real â nat. âFi::nat â real â 'a. (âi. P -` {i} â sets real_borel) â¶ (âi. Fi i â Mx) â¶ (λr. Fi (P r) r) â Mx)" lemma separate_measurable: fixes P :: "real â nat" assumes "âi. P -` {i} â sets real_borel" shows "P â real_borel ââ©M nat_borel" proof - have "P â real_borel ââ©M count_space UNIV" by (auto simp add: assms measurable_count_space_eq_countable) thus ?thesis using measurable_cong_sets sets_borel_eq_count_space by blast qed lemma measurable_separate: fixes P :: "real â nat" assumes "P â real_borel ââ©M nat_borel" shows "P -` {i} â sets real_borel" by(rule measurable_sets_borel[OF assms borel_singleton[OF sets.empty_sets,of i]]) definition "is_quasi_borel X Mx â· Mx â UNIV â X â§ qbs_closed1 Mx â§ qbs_closed2 X Mx â§ qbs_closed3 Mx" lemma is_quasi_borel_intro[simp]: assumes "Mx â UNIV â X" and "qbs_closed1 Mx" "qbs_closed2 X Mx" "qbs_closed3 Mx" shows "is_quasi_borel X Mx" using assms by(simp add: is_quasi_borel_def) typedef 'a quasi_borel = "{(X::'a set, Mx). is_quasi_borel X Mx}" proof show "(UNIV, UNIV) â {(X::'a set, Mx). is_quasi_borel X Mx}" by (simp add: is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def) qed definition qbs_space :: "'a quasi_borel â 'a set" where "qbs_space X â¡ fst (Rep_quasi_borel X)" definition qbs_Mx :: "'a quasi_borel â (real â 'a) set" where "qbs_Mx X â¡ snd (Rep_quasi_borel X)" lemma qbs_decomp : "(qbs_space X,qbs_Mx X) â {(X::'a set, Mx). is_quasi_borel X Mx}" by (simp add: qbs_space_def qbs_Mx_def Rep_quasi_borel[simplified]) lemma qbs_Mx_to_X[dest]: assumes "α â qbs_Mx X" shows "α â UNIV â qbs_space X" "α r â qbs_space X" using qbs_decomp assms by(auto simp: is_quasi_borel_def) lemma qbs_closed1I: assumes "âα f. α â Mx â¹ f â real_borel ââ©M real_borel ⹠α â f â Mx" shows "qbs_closed1 Mx" using assms by(simp add: qbs_closed1_def) lemma qbs_closed1_dest[simp]: assumes "α â qbs_Mx X" and "f â real_borel ââ©M real_borel" shows "α â f â qbs_Mx X" using assms qbs_decomp by (auto simp add: is_quasi_borel_def qbs_closed1_def) lemma qbs_closed2I: assumes "âx. x â X â¹ (λr. x) â Mx" shows "qbs_closed2 X Mx" using assms by(simp add: qbs_closed2_def) lemma qbs_closed2_dest[simp]: assumes "x â qbs_space X" shows "(λr. x) â qbs_Mx X" using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed2_def) lemma qbs_closed3I: assumes "â(P :: real â nat) Fi. (âi. P -` {i} â sets real_borel) â¹ (âi. Fi i â Mx) â¹ (λr. Fi (P r) r) â Mx" shows "qbs_closed3 Mx" using assms by(auto simp: qbs_closed3_def) lemma qbs_closed3I': assumes "â(P :: real â nat) Fi. P â real_borel ââ©M nat_borel â¹ (âi. Fi i â Mx) â¹ (λr. Fi (P r) r) â Mx" shows "qbs_closed3 Mx" using assms by(auto intro!: qbs_closed3I simp: separate_measurable) lemma qbs_closed3_dest[simp]: fixes P::"real â nat" and Fi :: "nat â real â _" assumes "âi. P -` {i} â sets real_borel" and "âi. Fi i â qbs_Mx X" shows "(λr. Fi (P r) r) â qbs_Mx X" using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed3_def) lemma qbs_closed3_dest': fixes P::"real â nat" and Fi :: "nat â real â _" assumes "P â real_borel ââ©M nat_borel" and "âi. Fi i â qbs_Mx X" shows "(λr. Fi (P r) r) â qbs_Mx X" using qbs_closed3_dest[OF measurable_separate[OF assms(1)] assms(2)] . lemma qbs_closed3_dest2: assumes "countable I" and [measurable]: "P â real_borel ââ©M count_space I" and "âi. i â I â¹ Fi i â qbs_Mx X" shows "(λr. Fi (P r) r) â qbs_Mx X" proof - have 0:"I â {}" using measurable_empty_iff[of "count_space I" P real_borel] assms(2) by fastforce define P' where "P' â¡ to_nat_on I â P" define Fi' where "Fi' â¡ Fi â (from_nat_into I)" have 1:"P' â real_borel ââ©M nat_borel" by(simp add: P'_def) have 2:"âi. Fi' i â qbs_Mx X" using assms(3) from_nat_into[OF 0] by(simp add: Fi'_def) have "(λr. Fi' (P' r) r) â qbs_Mx X" using 1 2 measurable_separate by auto thus ?thesis using from_nat_into_to_nat_on[OF assms(1)] measurable_space[OF assms(2)] by(auto simp: Fi'_def P'_def) qed lemma qbs_closed3_dest2': assumes "countable I" and [measurable]: "P â real_borel ââ©M count_space I" and "âi. i â range P â¹ Fi i â qbs_Mx X" shows "(λr. Fi (P r) r) â qbs_Mx X" proof - have 0:"range P â© I = range P" using measurable_space[OF assms(2)] by auto have 1:"P â real_borel ââ©M count_space (range P)" using restrict_count_space[of I "range P"] measurable_restrict_space2[OF _ assms(2),of "range P"] by(simp add: 0) have 2:"countable (range P)" using countable_Int2[OF assms(1),of "range P"] by(simp add: 0) show ?thesis by(auto intro!: qbs_closed3_dest2[OF 2 1 assms(3)]) qed lemma qbs_space_Mx: "qbs_space X = {α x |x α. α â qbs_Mx X}" proof auto fix x assume 1:"x â qbs_space X" show "âxa α. x = α xa ⧠α â qbs_Mx X" by(auto intro!: exI[where x=0] exI[where x="(λr. x)"] simp: 1) qed lemma qbs_space_eq_Mx: assumes "qbs_Mx X = qbs_Mx Y" shows "qbs_space X = qbs_space Y" by(simp add: qbs_space_Mx assms) lemma qbs_eqI: assumes "qbs_Mx X = qbs_Mx Y" shows "X = Y" by (metis Rep_quasi_borel_inverse prod.exhaust_sel qbs_Mx_def qbs_space_def assms qbs_space_eq_Mx[OF assms]) subsubsection â¹ Morphism of Quasi-Borel Spaces ⺠definition qbs_morphism :: "['a quasi_borel, 'b quasi_borel] â ('a â 'b) set" (infixr "ââ©Q" 60) where "X ââ©Q Y â¡ {f â qbs_space X â qbs_space Y. âα â qbs_Mx X. f â α â qbs_Mx Y}" lemma qbs_morphismI: assumes "âα. α â qbs_Mx X â¹ f â α â qbs_Mx Y" shows "f â X ââ©Q Y" proof - have "f â qbs_space X â qbs_space Y" proof fix x assume "x â qbs_space X " then have "(λr. x) â qbs_Mx X" by simp hence "f â (λr. x) â qbs_Mx Y" using assms by blast thus "f x â qbs_space Y" by auto qed thus ?thesis using assms by(simp add: qbs_morphism_def) qed lemma qbs_morphismE[dest]: assumes "f â X ââ©Q Y" shows "f â qbs_space X â qbs_space Y" "âx. x â qbs_space X â¹ f x â qbs_space Y" "âα. α â qbs_Mx X â¹ f â α â qbs_Mx Y" using assms by(auto simp add: qbs_morphism_def) lemma qbs_morphism_ident[simp]: "id â X ââ©Q X" by(auto intro: qbs_morphismI) lemma qbs_morphism_ident'[simp]: "(λx. x) â X ââ©Q X" using qbs_morphism_ident by(simp add: id_def) lemma qbs_morphism_comp: assumes "f â X ââ©Q Y" "g â Y ââ©Q Z" shows "g â f â X ââ©Q Z" using assms by (simp add: comp_assoc Pi_def qbs_morphism_def) lemma qbs_morphism_cong: assumes "âx. x â qbs_space X â¹ f x = g x" and "f â X ââ©Q Y" shows "g â X ââ©Q Y" proof(rule qbs_morphismI) fix α assume 1:"α â qbs_Mx X" have "g â α = f â α" proof fix x have "α x â qbs_space X" using 1 qbs_decomp[of X] by auto thus "(g â α) x = (f â α) x" using assms(1) by simp qed thus "g â α â qbs_Mx Y" using 1 assms(2) by(simp add: qbs_morphism_def) qed lemma qbs_morphism_const: assumes "y â qbs_space Y" shows "(λ_. y) â X ââ©Q Y" using assms by (auto intro: qbs_morphismI) subsubsection â¹ Empty Space ⺠definition empty_quasi_borel :: "'a quasi_borel" where "empty_quasi_borel â¡ Abs_quasi_borel ({},{})" lemma eqb_correct: "Rep_quasi_borel empty_quasi_borel = ({}, {})" using Abs_quasi_borel_inverse by(auto simp add: Abs_quasi_borel_inverse empty_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def) lemma eqb_space[simp]: "qbs_space empty_quasi_borel = {}" by(simp add: qbs_space_def eqb_correct) lemma eqb_Mx[simp]: "qbs_Mx empty_quasi_borel = {}" by(simp add: qbs_Mx_def eqb_correct) lemma qbs_empty_equiv :"qbs_space X = {} â· qbs_Mx X = {}" proof(auto) fix x assume "qbs_Mx X = {}" and h:"x â qbs_space X" have "(λr. x) â qbs_Mx X" using h by simp thus "False" using â¹qbs_Mx X = {}⺠by simp qed lemma empty_quasi_borel_iff: "qbs_space X = {} â· X = empty_quasi_borel" by(auto intro!: qbs_eqI) subsubsection â¹ Unit Space ⺠definition unit_quasi_borel :: "unit quasi_borel" ("1â©Q") where "unit_quasi_borel â¡ Abs_quasi_borel (UNIV,UNIV)" lemma uqb_correct: "Rep_quasi_borel unit_quasi_borel = (UNIV,UNIV)" using Abs_quasi_borel_inverse by(auto simp add: unit_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def) lemma uqb_space[simp]: "qbs_space unit_quasi_borel = {()}" by(simp add: qbs_space_def UNIV_unit uqb_correct) lemma uqb_Mx[simp]: "qbs_Mx unit_quasi_borel = {λr. ()}" by(auto simp add: qbs_Mx_def uqb_correct) lemma unit_quasi_borel_terminal: "â! f. f â X ââ©Q unit_quasi_borel" by(fastforce simp: qbs_morphism_def) definition to_unit_quasi_borel :: "'a â unit" ("!â©Q") where "to_unit_quasi_borel â¡ (λ_.())" lemma to_unit_quasi_borel_morphism : "!â©Q â X ââ©Q unit_quasi_borel" by(auto simp add: to_unit_quasi_borel_def qbs_morphism_def) subsubsection â¹ Subspaces ⺠definition sub_qbs :: "['a quasi_borel, 'a set] â 'a quasi_borel" where "sub_qbs X U â¡ Abs_quasi_borel (qbs_space X â© U,{f â UNIV â qbs_space X â© U. f â qbs_Mx X})" lemma sub_qbs_closed: "qbs_closed1 {f â UNIV â qbs_space X â© U. f â qbs_Mx X}" "qbs_closed2 (qbs_space X â© U) {f â UNIV â qbs_space X â© U. f â qbs_Mx X}" "qbs_closed3 {f â UNIV â qbs_space X â© U. f â qbs_Mx X}" unfolding qbs_closed1_def qbs_closed2_def qbs_closed3_def by auto lemma sub_qbs_correct[simp]: "Rep_quasi_borel (sub_qbs X U) = (qbs_space X â© U,{f â UNIV â qbs_space X â© U. f â qbs_Mx X})" by(simp add: Abs_quasi_borel_inverse sub_qbs_def sub_qbs_closed) lemma sub_qbs_space[simp]: "qbs_space (sub_qbs X U) = qbs_space X â© U" by(simp add: qbs_space_def) lemma sub_qbs_Mx[simp]: "qbs_Mx (sub_qbs X U) = {f â UNIV â qbs_space X â© U. f â qbs_Mx X}" by(simp add: qbs_Mx_def) lemma sub_qbs: assumes "U â qbs_space X" shows "(qbs_space (sub_qbs X U), qbs_Mx (sub_qbs X U)) = (U, {f â UNIV â U. f â qbs_Mx X})" using assms by auto subsubsection â¹ Image Spaces ⺠definition map_qbs :: "['a â 'b] â 'a quasi_borel â 'b quasi_borel" where "map_qbs f X = Abs_quasi_borel (f ` (qbs_space X),{β. âαâ qbs_Mx X. β = f â α})" lemma map_qbs_f: "{β. âαâ qbs_Mx X. β = f â α} â UNIV â f ` (qbs_space X)" by fastforce lemma map_qbs_closed1: "qbs_closed1 {β. âαâ qbs_Mx X. β = f â α}" unfolding qbs_closed1_def using qbs_closed1_dest by(fastforce simp: comp_def) lemma map_qbs_closed2: "qbs_closed2 (f ` (qbs_space X)) {β. âαâ qbs_Mx X. β = f â α}" unfolding qbs_closed2_def by fastforce lemma map_qbs_closed3: "qbs_closed3 {β. âαâ qbs_Mx X. β = f â α}" proof(auto simp add: qbs_closed3_def) fix P Fi assume h:"âi::nat. P -` {i} â sets real_borel" "âi::nat. âαâqbs_Mx X. Fi i = f â α" then obtain αi where ha: "âi::nat. αi i â qbs_Mx X â§ Fi i = f â (αi i)" by metis hence 1:"(λr. αi (P r) r) â qbs_Mx X" using h(1) by fastforce show "âαâqbs_Mx X. (λr. Fi (P r) r) = f â α" by(auto intro!: bexI[where x="(λr. αi (P r) r)"] simp add: 1 ha comp_def) qed lemma map_qbs_correct[simp]: "Rep_quasi_borel (map_qbs f X) = (f ` (qbs_space X),{β. âαâ qbs_Mx X. β = f â α})" unfolding map_qbs_def by(simp add: Abs_quasi_borel_inverse map_qbs_f map_qbs_closed1 map_qbs_closed2 map_qbs_closed3) lemma map_qbs_space[simp]: "qbs_space (map_qbs f X) = f ` (qbs_space X)" by(simp add: qbs_space_def) lemma map_qbs_Mx[simp]: "qbs_Mx (map_qbs f X) = {β. âαâ qbs_Mx X. β = f â α}" by(simp add: qbs_Mx_def) inductive_set generating_Mx :: "'a set â (real â 'a) set â (real â 'a) set" for X :: "'a set" and Mx :: "(real â 'a) set" where Basic: "α â Mx ⹠α â generating_Mx X Mx" | Const: "x â X â¹ (λr. x) â generating_Mx X Mx" | Comp : "f â real_borel ââ©M real_borel ⹠α â generating_Mx X Mx ⹠α â f â generating_Mx X Mx" | Part : "(âi. Fi i â generating_Mx X Mx) â¹ P â real_borel ââ©M nat_borel â¹ (λr. Fi (P r) r) â generating_Mx X Mx" lemma generating_Mx_to_space: assumes "Mx â UNIV â X" shows "generating_Mx X Mx â UNIV â X" proof fix α assume "α â generating_Mx X Mx" then show "α â UNIV â X" by(induct rule: generating_Mx.induct) (use assms in auto) qed lemma generating_Mx_closed1: "qbs_closed1 (generating_Mx X Mx)" by (simp add: generating_Mx.Comp qbs_closed1I) lemma generating_Mx_closed2: "qbs_closed2 X (generating_Mx X Mx)" by (simp add: generating_Mx.Const qbs_closed2I) lemma generating_Mx_closed3: "qbs_closed3 (generating_Mx X Mx)" by(simp add: qbs_closed3I' generating_Mx.Part) lemma generating_Mx_Mx: "generating_Mx (qbs_space X) (qbs_Mx X) = qbs_Mx X" proof auto fix α assume "α â generating_Mx (qbs_space X) (qbs_Mx X)" then show "α â qbs_Mx X" by(rule generating_Mx.induct) (auto intro!: qbs_closed1_dest[simplified comp_def] simp: qbs_closed3_dest') next fix α assume "α â qbs_Mx X" then show "α â generating_Mx (qbs_space X) (qbs_Mx X)" .. qed subsubsection â¹ Ordering of Quasi-Borel Spaces ⺠instantiation quasi_borel :: (type) order_bot begin inductive less_eq_quasi_borel :: "'a quasi_borel â 'a quasi_borel â bool" where "qbs_space X â qbs_space Y â¹ less_eq_quasi_borel X Y" | "qbs_space X = qbs_space Y â¹ qbs_Mx Y â qbs_Mx X â¹ less_eq_quasi_borel X Y" lemma le_quasi_borel_iff: "X ⤠Y â· (if qbs_space X = qbs_space Y then qbs_Mx Y â qbs_Mx X else qbs_space X â qbs_space Y)" by(auto elim: less_eq_quasi_borel.cases intro: less_eq_quasi_borel.intros) definition less_quasi_borel :: "'a quasi_borel â 'a quasi_borel â bool" where "less_quasi_borel X Y â· (X ⤠Y ⧠¬ Y ⤠X)" definition bot_quasi_borel :: "'a quasi_borel" where "bot_quasi_borel = empty_quasi_borel" instance proof show "bot ⤠a" for a :: "'a quasi_borel" using qbs_empty_equiv by(auto simp add: le_quasi_borel_iff bot_quasi_borel_def) qed (auto simp: le_quasi_borel_iff less_quasi_borel_def split: if_split_asm intro: qbs_eqI) end definition inf_quasi_borel :: "['a quasi_borel, 'a quasi_borel] â 'a quasi_borel" where "inf_quasi_borel X X' = Abs_quasi_borel (qbs_space X â© qbs_space X', qbs_Mx X â© qbs_Mx X')" lemma inf_quasi_borel_correct: "Rep_quasi_borel (inf_quasi_borel X X') = (qbs_space X â© qbs_space X', qbs_Mx X â© qbs_Mx X')" by(fastforce intro!: Abs_quasi_borel_inverse simp: inf_quasi_borel_def is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def) lemma inf_qbs_space[simp]: "qbs_space (inf_quasi_borel X X') = qbs_space X â© qbs_space X'" by (simp add: qbs_space_def inf_quasi_borel_correct) lemma inf_qbs_Mx[simp]: "qbs_Mx (inf_quasi_borel X X') = qbs_Mx X â© qbs_Mx X'" by(simp add: qbs_Mx_def inf_quasi_borel_correct) definition max_quasi_borel :: "'a set â 'a quasi_borel" where "max_quasi_borel X = Abs_quasi_borel (X, UNIV â X)" lemma max_quasi_borel_correct: "Rep_quasi_borel (max_quasi_borel X) = (X, UNIV â X)" by(fastforce intro!: Abs_quasi_borel_inverse simp: max_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def) lemma max_qbs_space[simp]: "qbs_space (max_quasi_borel X) = X" by(simp add: qbs_space_def max_quasi_borel_correct) lemma max_qbs_Mx[simp]: "qbs_Mx (max_quasi_borel X) = UNIV â X" by(simp add: qbs_Mx_def max_quasi_borel_correct) instantiation quasi_borel :: (type) semilattice_sup begin definition sup_quasi_borel :: "'a quasi_borel â 'a quasi_borel â 'a quasi_borel" where "sup_quasi_borel X Y â¡ (if qbs_space X = qbs_space Y then inf_quasi_borel X Y else if qbs_space X â qbs_space Y then Y else if qbs_space Y â qbs_space X then X else max_quasi_borel (qbs_space X ⪠qbs_space Y))" instance proof fix X Y :: "'a quasi_borel" let ?X = "qbs_space X" let ?Y = "qbs_space Y" consider "?X = ?Y" | "?X â ?Y" | "?Y â ?X" | "?X â ?X ⪠?Y â§ ?Y â ?X ⪠?Y" by auto then show "X ⤠X â Y" proof(cases) case 1 show ?thesis unfolding sup_quasi_borel_def by(rule less_eq_quasi_borel.intros(2),simp_all add: 1) next case 2 then show ?thesis unfolding sup_quasi_borel_def by (simp add: less_eq_quasi_borel.intros(1)) next case 3 then show ?thesis unfolding sup_quasi_borel_def by auto next case 4 then show ?thesis unfolding sup_quasi_borel_def by(auto simp: less_eq_quasi_borel.intros(1)) qed next fix X Y :: "'a quasi_borel" let ?X = "qbs_space X" let ?Y = "qbs_space Y" consider "?X = ?Y" | "?X â ?Y" | "?Y â ?X" | "?X â ?X ⪠?Y â§ ?Y â ?X ⪠?Y" by auto then show "Y ⤠X â Y" proof(cases) case 1 show ?thesis unfolding sup_quasi_borel_def by(rule less_eq_quasi_borel.intros(2)) (simp_all add: 1) next case 2 then show ?thesis unfolding sup_quasi_borel_def by auto next case 3 then show ?thesis unfolding sup_quasi_borel_def by (auto simp add: less_eq_quasi_borel.intros(1)) next case 4 then show ?thesis unfolding sup_quasi_borel_def by(auto simp: less_eq_quasi_borel.intros(1)) qed next fix X Y Z :: "'a quasi_borel" assume h:"X ⤠Z" "Y ⤠Z" let ?X = "qbs_space X" let ?Y = "qbs_space Y" let ?Z = "qbs_space Z" consider "?X = ?Y" | "?X â ?Y" | "?Y â ?X" | "?X â ?X ⪠?Y â§ ?Y â ?X ⪠?Y" by auto then show "sup X Y ⤠Z" proof cases case 1 show ?thesis unfolding sup_quasi_borel_def apply(simp add: 1,rule less_eq_quasi_borel.cases[OF h(1)]) apply(rule less_eq_quasi_borel.intros(1)) apply auto[1] apply auto apply(rule less_eq_quasi_borel.intros(2)) apply(simp add: 1) by(rule less_eq_quasi_borel.cases[OF h(2)]) (auto simp: 1) next case 2 then show ?thesis unfolding sup_quasi_borel_def using h(2) by auto next case 3 then show ?thesis unfolding sup_quasi_borel_def using h(1) by auto next case 4 then have [simp]:"?X â ?Y" "~ (?X â ?Y)" "~ (?Y â ?X)" by auto have [simp]:"?X â ?Z" "?Y â ?Z" by (metis h(1) dual_order.order_iff_strict less_eq_quasi_borel.cases) (metis h(2) dual_order.order_iff_strict less_eq_quasi_borel.cases) then consider "?X ⪠?Y = ?Z" | "?X ⪠?Y â ?Z" by blast then show ?thesis unfolding sup_quasi_borel_def apply cases apply simp apply(rule less_eq_quasi_borel.intros(2)) apply simp apply auto[1] by(simp add: less_eq_quasi_borel.intros(1)) qed qed end end
le>
Theory Measure_QuasiBorel_Adjunction
(* Title: Measure_QuasiBorel_Adjunction.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) subsection â¹Relation to Measurable Spaces⺠theory Measure_QuasiBorel_Adjunction imports "QuasiBorel" begin text â¹ We construct the adjunction between \textbf{Meas} and \textbf{QBS}, where \textbf{Meas} is the category of measurable spaces and measurable functions and \textbf{QBS} is the category of quasi-Borel spaces and morphisms.⺠subsubsection â¹ The Functor $R$ ⺠definition measure_to_qbs :: "'a measure â 'a quasi_borel" where "measure_to_qbs X â¡ Abs_quasi_borel (space X, real_borel ââ©M X)" lemma R_Mx_correct: "real_borel ââ©M X â UNIV â space X" by (simp add: measurable_space subsetI) lemma R_qbs_closed1: "qbs_closed1 (real_borel ââ©M X)" by (simp add: qbs_closed1_def) lemma R_qbs_closed2: "qbs_closed2 (space X) (real_borel ââ©M X)" by (simp add: qbs_closed2_def) lemma R_qbs_closed3: "qbs_closed3 (real_borel ââ©M (X :: 'a measure))" proof(rule qbs_closed3I) fix P::"real â nat" fix Fi::"nat â real â 'a" assume h:"âi. P -` {i} â sets real_borel" "âi. Fi i â real_borel ââ©M X" show "(λr. Fi (P r) r) â real_borel ââ©M X" proof(rule measurableI) fix x assume "x â space real_borel" then show "Fi (P x) x â space X" using h(2) measurable_space[of "Fi (P x)" real_borel X x] by auto next fix A assume h':"A â sets X" have "(λr. Fi (P r) r) -` A = (âi::nat. ((Fi i -` A) â© (P -` {i})))" by auto also have "... â sets real_borel" using sets.Int measurable_sets[OF h(2) h'] h(1) by(auto intro!: countable_Un_Int(1)) finally show "(λr. Fi (P r) r) -` A â© space real_borel â sets real_borel" by simp qed qed lemma R_correct[simp]: "Rep_quasi_borel (measure_to_qbs X) = (space X, real_borel ââ©M X)" unfolding measure_to_qbs_def by (rule Abs_quasi_borel_inverse) (simp add: R_Mx_correct R_qbs_closed1 R_qbs_closed2 R_qbs_closed3) lemma qbs_space_R[simp]: "qbs_space (measure_to_qbs X) = space X" by (simp add: qbs_space_def) lemma qbs_Mx_R[simp]: "qbs_Mx (measure_to_qbs X) = real_borel ââ©M X" by (simp add: qbs_Mx_def) text â¹ The following lemma says that @{term measure_to_qbs} is a functor from \textbf{Meas} to \textbf{QBS}. ⺠lemma r_preserves_morphisms: "X ââ©M Y â (measure_to_qbs X) ââ©Q (measure_to_qbs Y)" by(auto intro!: qbs_morphismI) subsubsection â¹ The Functor $L$ ⺠definition sigma_Mx :: "'a quasi_borel â 'a set set" where "sigma_Mx X â¡ {U â© qbs_space X |U. âαâqbs_Mx X. α -` U â sets real_borel}" definition qbs_to_measure :: "'a quasi_borel â 'a measure" where "qbs_to_measure X â¡ Abs_measure (qbs_space X, sigma_Mx X, λA. (if A = {} then 0 else if A â - sigma_Mx X then 0 else â))" lemma measure_space_L: "measure_space (qbs_space X) (sigma_Mx X) (λA. (if A = {} then 0 else if A â - sigma_Mx X then 0 else â))" unfolding measure_space_def proof auto show "sigma_algebra (qbs_space X) (sigma_Mx X)" proof(rule sigma_algebra.intro) show "algebra (qbs_space X) (sigma_Mx X)" proof have "â U â sigma_Mx X. U â qbs_space X" using sigma_Mx_def subset_iff by fastforce thus "sigma_Mx X â Pow (qbs_space X)" by auto next show "{} â sigma_Mx X" unfolding sigma_Mx_def by auto next fix A fix B assume "A â sigma_Mx X" "B â sigma_Mx X" then have "â Ua. A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)" by (simp add: sigma_Mx_def) then obtain Ua where pa:"A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)" by auto have "â Ub. B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)" using â¹B â sigma_Mx X⺠sigma_Mx_def by auto then obtain Ub where pb:"B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)" by auto from pa pb have [simp]:"âαâqbs_Mx X. α -` (Ua â© Ub) â sets real_borel" by auto from this pa pb sigma_Mx_def have [simp]:"(Ua â© Ub) â© qbs_space X â sigma_Mx X" by blast from pa pb have [simp]:"A â© B = (Ua â© Ub) â© qbs_space X" by auto thus "A â© B â sigma_Mx X" by simp next fix A fix B assume "A â sigma_Mx X" "B â sigma_Mx X" then have "â Ua. A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)" by (simp add: sigma_Mx_def) then obtain Ua where pa:"A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)" by auto have "â Ub. B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)" using â¹B â sigma_Mx X⺠sigma_Mx_def by auto then obtain Ub where pb:"B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)" by auto from pa pb have [simp]:"A - B = (Ua â© -Ub) â© qbs_space X" by auto from pa pb have "âαâqbs_Mx X. α -`(Ua â© -Ub) â sets real_borel" by (metis Diff_Compl double_compl sets.Diff vimage_Compl vimage_Int) hence 1:"A - B â sigma_Mx X" using sigma_Mx_def â¹A - B = Ua â© - Ub â© qbs_space X⺠by blast show "âCâsigma_Mx X. finite C â§ disjoint C â§ A - B = â C" proof show "{A - B} âsigma_Mx X â§ finite {A-B} â§ disjoint {A-B} â§ A - B = â {A-B}" using 1 by auto qed next fix A fix B assume "A â sigma_Mx X" "B â sigma_Mx X" then have "â Ua. A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)" by (simp add: sigma_Mx_def) then obtain Ua where pa:"A = Ua â© qbs_space X â§ (âαâqbs_Mx X. α -` Ua â sets real_borel)" by auto have "â Ub. B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)" using â¹B â sigma_Mx X⺠sigma_Mx_def by auto then obtain Ub where pb:"B = Ub â© qbs_space X â§ (âαâqbs_Mx X. α -` Ub â sets real_borel)" by auto from pa pb have "A ⪠B = (Ua ⪠Ub) â© qbs_space X" by auto from pa pb have "âαâqbs_Mx X. α -`(Ua ⪠Ub) â sets real_borel" by auto then show "A ⪠B â sigma_Mx X" unfolding sigma_Mx_def using â¹A ⪠B = (Ua ⪠Ub) â© qbs_space X⺠by blast next have "âαâqbs_Mx X. α -` (UNIV) â sets real_borel" by simp thus "qbs_space X â sigma_Mx X" unfolding sigma_Mx_def by blast qed next show "sigma_algebra_axioms (sigma_Mx X)" unfolding sigma_algebra_axioms_def proof(auto) fix A :: "nat â _" assume 1:"range A â sigma_Mx X" then have 2:"âi. âUi. A i = Ui â© qbs_space X â§ (âαâqbs_Mx X. α -` Ui â sets real_borel)" unfolding sigma_Mx_def by auto then have "â U :: nat â _. âi. A i = U i â© qbs_space X â§ (âαâqbs_Mx X. α -` (U i) â sets real_borel)" by (rule choice) from this obtain U where pu:"âi. A i = U i â© qbs_space X â§ (âαâqbs_Mx X. α -` (U i) â sets real_borel)" by auto hence "âαâqbs_Mx X. α -` (â (range U)) â sets real_borel" by (simp add: countable_Un_Int(1) vimage_UN) from pu have "â (range A) = (âi::nat. (U i â© qbs_space X))" by blast hence "â (range A) = â (range U) â© qbs_space X" by auto thus "â (range A) â sigma_Mx X" using sigma_Mx_def â¹âαâqbs_Mx X. α -` â (range U) â sets real_borel⺠by blast qed qed next show "countably_additive (sigma_Mx X) (λA. if A = {} then 0 else if A â - sigma_Mx X then 0 else â)" proof(rule countably_additiveI) fix A :: "nat â _" assume h:"range A â sigma_Mx X" "â (range A) â sigma_Mx X" consider "â (range A) = {}" | "â (range A) â {}" by auto then show "(âi. if A i = {} then 0 else if A i â - sigma_Mx X then 0 else â) = (if â (range A) = {} then 0 else if â (range A) â - sigma_Mx X then 0 else (â :: ennreal))" proof cases case 1 then have "âi. A i = {}" by simp thus ?thesis by(simp add: 1) next case 2 then obtain j where hj:"A j â {}" by auto have "(âi. if A i = {} then 0 else if A i â - sigma_Mx X then 0 else â) = (â :: ennreal)" proof - have hsum:"âN f. sum f {..<N} ⤠(ân. (f n :: ennreal))" by (simp add: sum_le_suminf) have hsum':"âP f. (âj. j â P â§ f j = (â :: ennreal)) â¹ finite P â¹ sum f P = â" by auto have h1:"(âi<j+1. if A i = {} then 0 else if A i â - sigma_Mx X then 0 else â) = (â :: ennreal)" proof(rule hsum') show "âja. ja â {..<j + 1} â§ (if A ja = {} then 0 else if A ja â - sigma_Mx X then 0 else â) = (â :: ennreal)" proof(rule exI[where x=j],rule conjI) have "A j â sigma_Mx X" using h(1) by auto then show "(if A j = {} then 0 else if A j â - sigma_Mx X then 0 else â) = (â :: ennreal)" using hj by simp qed simp qed simp have "(âi<j+1. if A i = {} then 0 else if A i â - sigma_Mx X then 0 else â) ⤠(âi. if A i = {} then 0 else if A i â - sigma_Mx X then 0 else (â :: ennreal))" by(rule hsum) thus ?thesis by(simp only: h1) (simp add: top.extremum_unique) qed moreover have "(if â (range A) = {} then 0 else if â (range A) â - sigma_Mx X then 0 else â) = (â :: ennreal)" using 2 h(2) by simp ultimately show ?thesis by simp qed qed qed(simp add: positive_def) lemma L_correct[simp]:"Rep_measure (qbs_to_measure X) = (qbs_space X, sigma_Mx X, λA. (if A = {} then 0 else if A â - sigma_Mx X then 0 else â))" unfolding qbs_to_measure_def by(auto intro!: Abs_measure_inverse simp: measure_space_L) lemma space_L[simp]: "space (qbs_to_measure X) = qbs_space X" by (simp add: space_def) lemma sets_L[simp]: "sets (qbs_to_measure X) = sigma_Mx X" by (simp add: sets_def) lemma emeasure_L[simp]: "emeasure (qbs_to_measure X) = (λA. if A = {} ⨠A â sigma_Mx X then 0 else â)" by(auto simp: emeasure_def) lemma qbs_Mx_sigma_Mx_contra: assumes "qbs_space X = qbs_space Y" and "qbs_Mx X â qbs_Mx Y" shows "sigma_Mx Y â sigma_Mx X" using assms by(auto simp: sigma_Mx_def) text â¹ The following lemma says that @{term qbs_to_measure} is a functor from \textbf{QBS} to \textbf{Meas}. ⺠lemma l_preserves_morphisms: "X ââ©Q Y â (qbs_to_measure X) ââ©M (qbs_to_measure Y)" proof(auto) fix f assume h:"f â X ââ©Q Y" show "f â (qbs_to_measure X) ââ©M (qbs_to_measure Y)" proof(rule measurableI) fix x assume "x â space (qbs_to_measure X)" then show "f x â space (qbs_to_measure Y)" using h by auto next fix A assume "A â sets (qbs_to_measure Y)" then obtain Ua where pa:"A = Ua â© qbs_space Y â§ (âαâqbs_Mx Y. α -` Ua â sets real_borel)" by (auto simp: sigma_Mx_def) have "âαâqbs_Mx X. f â α â qbs_Mx Y" "âαâ qbs_Mx X. α -` (f -` (qbs_space Y)) = UNIV" using h by auto hence "âαâqbs_Mx X. α -` (f -` A) = α -` (f -` Ua)" by (simp add: pa) from pa this qbs_morphism_def have "âαâqbs_Mx X. α -` (f -` A) â sets real_borel" by (simp add: vimage_comp â¹âαâqbs_Mx X. f â α â qbs_Mx Yâº) thus "f -` A â© space (qbs_to_measure X) â sets (qbs_to_measure X)" using sigma_Mx_def by auto qed qed abbreviation "qbs_borel â¡ measure_to_qbs borel" declare [[coercion measure_to_qbs]] abbreviation real_quasi_borel :: "real quasi_borel" ("ââ©Q") where "real_quasi_borel â¡ qbs_borel" abbreviation nat_quasi_borel :: "nat quasi_borel" ("ââ©Q") where "nat_quasi_borel â¡ qbs_borel" abbreviation ennreal_quasi_borel :: "ennreal quasi_borel" ("ââ©Qâ©â¥â©0") where "ennreal_quasi_borel â¡ qbs_borel" abbreviation bool_quasi_borel :: "bool quasi_borel" ("ð¹â©Q") where "bool_quasi_borel â¡ qbs_borel" lemma qbs_Mx_is_morphisms: "qbs_Mx X = real_quasi_borel ââ©Q X" proof(auto) fix α assume "α â qbs_Mx X" then have "α â UNIV â qbs_space X â§ (â f â real_borel ââ©M real_borel. α â f â qbs_Mx X)" by fastforce thus "α â real_quasi_borel ââ©Q X" by(simp add: qbs_morphism_def) next fix α assume "α â real_quasi_borel ââ©Q X" have "id â qbs_Mx real_quasi_borel" by simp then have "α â id â qbs_Mx X" using â¹Î± â real_quasi_borel ââ©Q X⺠qbs_morphism_def[of real_quasi_borel X] by blast then show "α â qbs_Mx X" by simp qed lemma qbs_Mx_subset_of_measurable: "qbs_Mx X â real_borel ââ©M qbs_to_measure X" proof fix α assume "α â qbs_Mx X" show "α â real_borel ââ©M qbs_to_measure X" proof(rule measurableI) fix x show "α x â space (qbs_to_measure X)" using qbs_decomp â¹Î± â qbs_Mx X⺠by auto next fix A assume "A â sets (qbs_to_measure X)" then have "α -`(qbs_space X) = UNIV" using â¹Î± â qbs_Mx X⺠qbs_decomp by auto then show "α -` A â© space real_borel â sets real_borel" using â¹Î± â qbs_Mx X⺠â¹A â sets (qbs_to_measure X)⺠by(auto simp add: sigma_Mx_def) qed qed lemma L_max_of_measurables: assumes "space M = qbs_space X" and "qbs_Mx X â real_borel ââ©M M" shows "sets M â sets (qbs_to_measure X)" proof fix U assume "U â sets M" from sets.sets_into_space[OF this] in_mono[OF assms(2)] measurable_sets_borel[OF _ this] show "U â sets (qbs_to_measure X)" using assms(1) by(auto intro!: exI[where x=U] simp: sigma_Mx_def) qed lemma qbs_Mx_are_measurable[simp,measurable]: assumes "α â qbs_Mx X" shows "α â real_borel ââ©M qbs_to_measure X" using assms qbs_Mx_subset_of_measurable by auto lemma measure_to_qbs_cong_sets: assumes "sets M = sets N" shows "measure_to_qbs M = measure_to_qbs N" by(rule qbs_eqI) (simp add: measurable_cong_sets[OF _ assms]) lemma lr_sets[simp,measurable_cong]: "sets X â sets (qbs_to_measure (measure_to_qbs X))" proof auto fix U assume "U â sets X" then have "U â© space X = U" by simp moreover have "âαâreal_borel ââ©M X. α -` U â sets real_borel" using â¹U â sets X⺠by(auto simp add: measurable_def) ultimately show "U â sigma_Mx (measure_to_qbs X)" by(auto simp add: sigma_Mx_def) qed lemma(in standard_borel) standard_borel_lr_sets_ident[simp, measurable_cong]: "sets (qbs_to_measure (measure_to_qbs M)) = sets M" proof auto fix V assume "V â sigma_Mx (measure_to_qbs M)" then obtain U where H2: "V = U â© space M â§ (âαâreal_borel ââ©M M. α -` U â sets real_borel)" by(auto simp: sigma_Mx_def) hence "g -` V = g -` (U â© space M)" by auto have "... = g -` U" using g_meas by(auto simp add: measurable_def) hence "f -` g -` U â© space M â sets M" by (meson f_meas g_meas measurable_sets H2) moreover have "f -` g -` U â© space M = U â© space M" by auto ultimately show "V â sets M" using H2 by simp next fix U assume "U â sets M" then show "U â sigma_Mx (measure_to_qbs M)" using lr_sets by auto qed subsubsection â¹ The Adjunction ⺠lemma lr_adjunction_correspondence : "X ââ©Q (measure_to_qbs Y) = (qbs_to_measure X) ââ©M Y" proof(auto) (* â *) fix f assume "f â X ââ©Q (measure_to_qbs Y)" show "f â qbs_to_measure X ââ©M Y" proof(rule measurableI) fix x assume "x â space (qbs_to_measure X)" hence "x â qbs_space X" by simp thus "f x â space Y" using â¹f â X ââ©Q (measure_to_qbs Y)⺠qbs_morphismE[of f X "measure_to_qbs Y"] by auto next fix A assume "A â sets Y" have "âα â qbs_Mx X. f â α â qbs_Mx (measure_to_qbs Y)" using â¹f â X ââ©Q (measure_to_qbs Y)⺠by auto hence "âα â qbs_Mx X. f â α â real_borel ââ©M Y" by simp hence "âα â qbs_Mx X. α -` (f -` A) â sets real_borel" using â¹Aâ sets Y⺠measurable_sets_borel vimage_comp by metis thus "f -` A â© space (qbs_to_measure X) â sets (qbs_to_measure X)" using sigma_Mx_def by auto qed (* â *) next fix f assume "f â qbs_to_measure X ââ©M Y" show "f â X ââ©Q measure_to_qbs Y" proof(rule qbs_morphismI,simp) fix α assume "α â qbs_Mx X" show "f â α â real_borel ââ©M Y" proof(rule measurableI) fix x assume "x â space real_borel" from this â¹Î± â qbs_Mx X âºqbs_decomp have "α x â qbs_space X" by auto hence "α x â space (qbs_to_measure X)" by simp thus "(f â α) x â space Y" using â¹f â qbs_to_measure X ââ©M Y⺠by (metis comp_def measurable_space) next fix A assume "A â sets Y" from â¹f â qbs_to_measure X ââ©M Y⺠measurable_sets this measurable_def have "f -` A â© space (qbs_to_measure X) â sets (qbs_to_measure X)" by blast hence "f -` A â© qbs_space X â sigma_Mx X" by simp then have "â V. f -` A â© qbs_space X = V â© qbs_space X â§ (âβâ qbs_Mx X. β -` V â sets real_borel)" by (simp add:sigma_Mx_def) then obtain V where h:"f -` A â© qbs_space X = V â© qbs_space X â§ (âβâ qbs_Mx X. β -` V â sets real_borel)" by auto have 1:"α -` (f -` A) = α -` (f -` A â© qbs_space X)" using â¹Î± â qbs_Mx X⺠by blast have 2:"α -` (V â© qbs_space X) = α -` V" using â¹Î± â qbs_Mx X⺠by blast from 1 2 h have "(f â α) -` A = α -` V" by (simp add: vimage_comp) from this h â¹Î± â qbs_Mx X âºshow "(f â α) -` A â© space real_borel â sets real_borel" by simp qed qed qed lemma(in standard_borel) standard_borel_r_full_faithful: "M ââ©M Y = measure_to_qbs M ââ©Q measure_to_qbs Y" proof(standard;standard) fix h assume "h â M ââ©M Y" then show "h â measure_to_qbs M ââ©Q measure_to_qbs Y" using r_preserves_morphisms by auto next fix h assume h:"h â measure_to_qbs M ââ©Q measure_to_qbs Y" show "h â M ââ©M Y" proof(rule measurableI) fix x assume "x â space M" then show "h x â space Y" using h by auto next fix U assume "U â sets Y" have "h â g â real_borel ââ©M Y" using â¹h â measure_to_qbs M ââ©Q measure_to_qbs Y⺠by(simp add: qbs_morphism_def) hence "(h â g) -` U â sets real_borel" by (simp add: â¹U â sets Y⺠measurable_sets_borel) hence "f -` ((h â g) -` U) â© space M â sets M" using f_meas in_borel_measurable_borel by blast moreover have "f -` ((h â g) -` U) â© space M = h -` U â© space M" using f_meas by auto ultimately show "h -` U â© space M â sets M" by simp qed qed lemma qbs_morphism_dest[dest]: assumes "f â X ââ©Q measure_to_qbs Y" shows "f â qbs_to_measure X ââ©M Y" using assms lr_adjunction_correspondence by auto lemma(in standard_borel) qbs_morphism_dest[dest]: assumes "k â measure_to_qbs M ââ©Q measure_to_qbs Y" shows "k â M ââ©M Y" using standard_borel_r_full_faithful assms by auto lemma qbs_morphism_measurable_intro[intro!]: assumes "f â qbs_to_measure X ââ©M Y" shows "f â X ââ©Q measure_to_qbs Y" using assms lr_adjunction_correspondence by auto lemma(in standard_borel) qbs_morphism_measurable_intro[intro!]: assumes "k â M ââ©M Y" shows "k â measure_to_qbs M ââ©Q measure_to_qbs Y" using standard_borel_r_full_faithful assms by auto text â¹ We can use the measurability prover when we reason about morphisms. ⺠lemma assumes "f â ââ©Q ââ©Q ââ©Q" shows "(λx. 2 * f x + (f x)^2) â ââ©Q ââ©Q ââ©Q" using assms by auto lemma assumes "f â X ââ©Q ââ©Q" and "α â qbs_Mx X" shows "(λx. 2 * f (α x) + (f (α x))^2) â ââ©Q ââ©Q ââ©Q" using assms by auto lemma qbs_morphisn_from_countable: fixes X :: "'a quasi_borel" assumes "countable (qbs_space X)" "qbs_Mx X â real_borel ââ©M count_space (qbs_space X)" and "âi. i â qbs_space X â¹ f i â qbs_space Y" shows "f â X ââ©Q Y" proof(rule qbs_morphismI) fix α assume "α â qbs_Mx X" then have [measurable]: "α â real_borel ââ©M count_space (qbs_space X)" using assms(2) .. define k :: "'a â real â _" where "k â¡ (λi _. f i)" have "f â α = (λr. k (α r) r)" by(auto simp add: k_def) also have "... â qbs_Mx Y" by(rule qbs_closed3_dest2[OF assms(1)]) (use assms(3) k_def in simp_all) finally show "f â α â qbs_Mx Y" . qed corollary nat_qbs_morphism: assumes "ân. f n â qbs_space Y" shows "f â ââ©Q ââ©Q Y" using assms measurable_cong_sets[OF refl sets_borel_eq_count_space,of real_borel] by(auto intro!: qbs_morphisn_from_countable) corollary bool_qbs_morphism: assumes "âb. f b â qbs_space Y" shows "f â ð¹â©Q ââ©Q Y" using assms measurable_cong_sets[OF refl sets_borel_eq_count_space,of real_borel] by(auto intro!: qbs_morphisn_from_countable) subsubsection â¹ The Adjunction w.r.t. Ordering⺠lemma l_mono: "mono qbs_to_measure" apply standard subgoal for X Y proof(induction rule: less_eq_quasi_borel.induct) case (1 X Y) then show ?case by(simp add: less_eq_measure.intros(1)) next case (2 X Y) then have "sigma_Mx X â sigma_Mx Y" by(auto simp add: sigma_Mx_def) then consider "sigma_Mx X â sigma_Mx Y" | "sigma_Mx X = sigma_Mx Y" by auto then show ?case apply(cases) apply(rule less_eq_measure.intros(2)) apply(simp_all add: 2) by(rule less_eq_measure.intros(3),simp_all add: 2) qed done lemma r_mono: "mono measure_to_qbs" apply standard subgoal for M N proof(induction rule: less_eq_measure.inducts) case (1 M N) then show ?case by(simp add: less_eq_quasi_borel.intros(1)) next case (2 M N) then have "real_borel ââ©M N â real_borel ââ©M M" by(simp add: measurable_mono) then consider "real_borel ââ©M N â real_borel ââ©M M" | "real_borel ââ©M N = real_borel ââ©M M" by auto then show ?case by cases (rule less_eq_quasi_borel.intros(2),simp_all add: 2)+ next case (3 M N) then show ?case apply - by(rule less_eq_quasi_borel.intros(2)) (simp_all add: measurable_mono) qed done lemma rl_order_adjunction: "X ⤠qbs_to_measure Y â· measure_to_qbs X ⤠Y" proof assume 1: "X ⤠qbs_to_measure Y" then show "measure_to_qbs X ⤠Y" proof(induction rule: less_eq_measure.cases) case (1 M N) then have [simp]:"qbs_space Y = space N" by(simp add: 1(2)[symmetric]) show ?case by(rule less_eq_quasi_borel.intros(1),simp add: 1) next case (2 M N) then have [simp]:"qbs_space Y = space N" by(simp add: 2(2)[symmetric]) show ?case proof(rule less_eq_quasi_borel.intros(2),simp add:2,auto) fix α assume h:"α â qbs_Mx Y" show "α â real_borel ââ©M X" proof(rule measurableI,simp_all) show "âx. α x â space X" using h by (auto simp add: 2) next fix A assume "A â sets X" then have "A â sets (qbs_to_measure Y)" using 2 by auto then obtain U where hu:"A = U â© space N" "(âαâqbs_Mx Y. α -` U â sets real_borel)" by(auto simp add: sigma_Mx_def) have "α -` A = α -` U" using h qbs_decomp[of Y] by(auto simp add: hu) thus "α -` A â sets borel" using h hu(2) by simp qed qed next case (3 M N) then have [simp]:"qbs_space Y = space N" by(simp add: 3(2)[symmetric]) show ?case proof(rule less_eq_quasi_borel.intros(2),simp add: 3,auto) fix α assume h:"α â qbs_Mx Y" show "α â real_borel ââ©M X" proof(rule measurableI,simp_all) show "âx. α x â space X" using h by(auto simp: 3) next fix A assume "A â sets X" then have "A â sets (qbs_to_measure Y)" using 3 by auto then obtain U where hu:"A = U â© space N" "(âαâqbs_Mx Y. α -` U â sets real_borel)" by(auto simp add: sigma_Mx_def) have "α -` A = α -` U" using h qbs_decomp[of Y] by(auto simp add: hu) thus "α -` A â sets borel" using h hu(2) by simp qed qed qed next assume "measure_to_qbs X ⤠Y" then show "X ⤠qbs_to_measure Y" proof(induction rule: less_eq_quasi_borel.cases) case (1 A B) have [simp]: "space X = qbs_space A" by(simp add: 1(1)[symmetric]) show ?case by(rule less_eq_measure.intros(1)) (simp add: 1) next case (2 A B) then have hmy:"qbs_Mx Y â real_borel ââ©M X" by auto have [simp]: "space X = qbs_space A" by(simp add: 2(1)[symmetric]) have "sets X â sigma_Mx Y" proof fix U assume hu:"U â sets X" show "U â sigma_Mx Y" proof(simp add: sigma_Mx_def,rule exI[where x=U],auto) show "âx. x â U â¹ x â qbs_space Y" using sets.sets_into_space[OF hu] by(auto simp add: 2) next fix α assume "α â qbs_Mx Y" then have "α â real_borel ââ©M X" using hmy by(auto) thus "α -` U â sets real_borel" using hu by(simp add: measurable_sets_borel) qed qed then consider "sets X = sigma_Mx Y" | "sets X â sigma_Mx Y" by auto then show ?case proof cases case 1 show ?thesis apply(rule less_eq_measure.intros(3),simp_all add: 1 2) proof(rule le_funI) fix U consider "U = {}" | "U â sigma_Mx B" | "U â {} â§ U â sigma_Mx B" by auto then show "emeasure X U ⤠(if U = {} ⨠U â sigma_Mx B then 0 else â)" proof cases case 1 then show ?thesis by simp next case h:2 then have "U â sigma_Mx A" using qbs_Mx_sigma_Mx_contra[OF 2(3)[symmetric] 2(4)] by auto hence "U â sets X" using lr_sets 2(1) by auto thus ?thesis by(simp add: h emeasure_notin_sets) next case 3 then show ?thesis by simp qed qed next case h2:2 show ?thesis by(rule less_eq_measure.intros(2)) (simp add: 2,simp add: h2) qed qed qed end
Theory Binary_Product_QuasiBorel
(* Title: Binary_Product_QuasiBorel.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) subsection â¹Product Spaces⺠theory Binary_Product_QuasiBorel imports "Measure_QuasiBorel_Adjunction" begin subsubsection â¹ Binary Product Spaces ⺠definition pair_qbs_Mx :: "['a quasi_borel, 'b quasi_borel] â (real => 'a à 'b) set" where "pair_qbs_Mx X Y â¡ {f. fst â f â qbs_Mx X â§ snd â f â qbs_Mx Y}" definition pair_qbs :: "['a quasi_borel, 'b quasi_borel] â ('a à 'b) quasi_borel" (infixr "â¨â©Q" 80) where "pair_qbs X Y = Abs_quasi_borel (qbs_space X à qbs_space Y, pair_qbs_Mx X Y)" lemma pair_qbs_f[simp]: "pair_qbs_Mx X Y â UNIV â qbs_space X à qbs_space Y" unfolding pair_qbs_Mx_def by (auto simp: mem_Times_iff[of _ "qbs_space X" "qbs_space Y"]; fastforce) lemma pair_qbs_closed1: "qbs_closed1 (pair_qbs_Mx (X::'a quasi_borel) (Y::'b quasi_borel))" unfolding pair_qbs_Mx_def qbs_closed1_def by (metis (no_types, lifting) comp_assoc mem_Collect_eq qbs_closed1_dest) lemma pair_qbs_closed2: "qbs_closed2 (qbs_space X à qbs_space Y) (pair_qbs_Mx X Y)" unfolding qbs_closed2_def pair_qbs_Mx_def by auto lemma pair_qbs_closed3: "qbs_closed3 (pair_qbs_Mx (X::'a quasi_borel) (Y::'b quasi_borel))" proof(auto simp add: qbs_closed3_def pair_qbs_Mx_def) fix P :: "real â nat" fix Fi :: "nat â real â 'a à 'b" define Fj :: "nat â real â 'a" where "Fj ⡠λj.(fst â Fi j)" assume "âi. fst â Fi i â qbs_Mx X â§ snd â Fi i â qbs_Mx Y" then have "âi. Fj i â qbs_Mx X" by (simp add: Fj_def) moreover assume "âi. P -` {i} â sets real_borel" ultimately have "(λr. Fj (P r) r) â qbs_Mx X" by auto moreover have "fst â (λr. Fi (P r) r) = (λr. Fj (P r) r)" by (auto simp add: Fj_def) ultimately show "fst â (λr. Fi (P r) r) â qbs_Mx X" by simp next fix P :: "real â nat" fix Fi :: "nat â real â 'a à 'b" define Fj :: "nat â real â 'b" where "Fj ⡠λj.(snd â Fi j)" assume "âi. fst â Fi i â qbs_Mx X â§ snd â Fi i â qbs_Mx Y" then have "âi. Fj i â qbs_Mx Y" by (simp add: Fj_def) moreover assume "âi. P -` {i} â sets real_borel" ultimately have "(λr. Fj (P r) r) â qbs_Mx Y" by auto moreover have "snd â (λr. Fi (P r) r) = (λr. Fj (P r) r)" by (auto simp add: Fj_def) ultimately show "snd â (λr. Fi (P r) r) â qbs_Mx Y" by simp qed lemma pair_qbs_correct: "Rep_quasi_borel (X â¨â©Q Y) = (qbs_space X à qbs_space Y, pair_qbs_Mx X Y)" unfolding pair_qbs_def by(auto intro!: Abs_quasi_borel_inverse pair_qbs_f simp: pair_qbs_closed3 pair_qbs_closed2 pair_qbs_closed1) lemma pair_qbs_space[simp]: "qbs_space (X â¨â©Q Y) = qbs_space X à qbs_space Y" by (simp add: qbs_space_def pair_qbs_correct) lemma pair_qbs_Mx[simp]: "qbs_Mx (X â¨â©Q Y) = pair_qbs_Mx X Y" by (simp add: qbs_Mx_def pair_qbs_correct) lemma pair_qbs_morphismI: assumes "âα β. α â qbs_Mx X ⹠β â qbs_Mx Y â¹ f â (λr. (α r, β r)) â qbs_Mx Z" shows "f â (X â¨â©Q Y) ââ©Q Z" proof(rule qbs_morphismI) fix α assume 1:"α â qbs_Mx (X â¨â©Q Y)" have "f â α = f â (λr. ((fst â α) r, (snd â α) r))" by auto also have "... â qbs_Mx Z" using 1 assms[of "fst â α" "snd â α"] by(simp add: pair_qbs_Mx_def) finally show "f â α â qbs_Mx Z" . qed lemma fst_qbs_morphism: "fst â X â¨â©Q Y ââ©Q X" by(auto simp add: qbs_morphism_def pair_qbs_Mx_def) lemma snd_qbs_morphism: "snd â X â¨â©Q Y ââ©Q Y" by(auto simp add: qbs_morphism_def pair_qbs_Mx_def) lemma qbs_morphism_pair_iff: "f â X ââ©Q Y â¨â©Q Z â· fst â f â X ââ©Q Y â§ snd â f â X ââ©Q Z" by(auto intro!: qbs_morphismI qbs_morphism_comp[OF _ fst_qbs_morphism,of f X Y Z ]qbs_morphism_comp[OF _ snd_qbs_morphism,of f X Y Z] simp: pair_qbs_Mx_def comp_assoc[symmetric]) lemma qbs_morphism_Pair1: assumes "x â qbs_space X" shows "Pair x â Y ââ©Q X â¨â©Q Y" using assms by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def comp_def) lemma qbs_morphism_Pair1': assumes "x â qbs_space X" and "f â X â¨â©Q Y ââ©Q Z" shows "(λy. f (x,y)) â Y ââ©Q Z" using qbs_morphism_comp[OF qbs_morphism_Pair1[OF assms(1)] assms(2)] by(simp add: comp_def) lemma qbs_morphism_Pair2: assumes "y â qbs_space Y" shows "(λx. (x,y)) â X ââ©Q X â¨â©Q Y" using assms by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def comp_def) lemma qbs_morphism_Pair2': assumes "y â qbs_space Y" and "f â X â¨â©Q Y ââ©Q Z" shows "(λx. f (x,y)) â X ââ©Q Z" using qbs_morphism_comp[OF qbs_morphism_Pair2[OF assms(1)] assms(2)] by(simp add: comp_def) lemma qbs_morphism_fst'': assumes "f â X ââ©Q Y" shows "(λk. f (fst k)) â X â¨â©Q Z ââ©Q Y" using qbs_morphism_comp[OF fst_qbs_morphism assms,of Z] by(simp add: comp_def) lemma qbs_morphism_snd'': assumes "f â X ââ©Q Y" shows "(λk. f (snd k)) â Z â¨â©Q X ââ©Q Y" using qbs_morphism_comp[OF snd_qbs_morphism assms,of Z] by(simp add: comp_def) lemma qbs_morphism_tuple: assumes "f â Z ââ©Q X" and "g â Z ââ©Q Y" shows "(λz. (f z, g z)) â Z ââ©Q X â¨â©Q Y" proof(rule qbs_morphismI,simp) fix α assume h:"α â qbs_Mx Z" then have "(λz. (f z, g z)) â α â UNIV â qbs_space X à qbs_space Y" using assms qbs_morphismE(2)[OF assms(1)] qbs_morphismE(2)[OF assms(2)] by fastforce moreover have "fst â ((λz. (f z, g z)) â α) = f â α" by auto moreover have "... â qbs_Mx X" using assms(1) h by auto moreover have "snd â ((λz. (f z, g z)) â α) = g â α" by auto moreover have "... â qbs_Mx Y" using assms(2) h by auto ultimately show "(λz. (f z, g z)) â α â pair_qbs_Mx X Y" by (simp add: pair_qbs_Mx_def) qed lemma qbs_morphism_map_prod: assumes "f â X ââ©Q Y" and "g â X' ââ©Q Y'" shows "map_prod f g â X â¨â©Q X'ââ©Q Y â¨â©Q Y'" proof(rule pair_qbs_morphismI) fix α β assume h:"α â qbs_Mx X" "β â qbs_Mx X'" have [simp]: "fst â (map_prod f g â (λr. (α r, β r))) = f â α" by auto have [simp]: "snd â (map_prod f g â (λr. (α r, β r))) = g â β" by auto show "map_prod f g â (λr. (α r, β r)) â qbs_Mx (Y â¨â©Q Y')" using h assms by(auto simp: pair_qbs_Mx_def) qed lemma qbs_morphism_pair_swap': "(λ(x,y). (y,x)) â (X::'a quasi_borel) â¨â©Q (Y::'b quasi_borel) ââ©Q Y â¨â©Q X" by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def split_beta' comp_def) lemma qbs_morphism_pair_swap: assumes "f â X â¨â©Q Y ââ©Q Z" shows "(λ(x,y). f (y,x)) â Y â¨â©Q X ââ©Q Z" proof - have "(λ(x,y). f (y,x)) = f â (λ(x,y). (y,x))" by auto thus ?thesis using qbs_morphism_comp[of "(λ(x,y). (y,x))" "Y â¨â©Q X" _ f] qbs_morphism_pair_swap' assms by auto qed lemma qbs_morphism_pair_assoc1: "(λ((x,y),z). (x,(y,z))) â (X â¨â©Q Y) â¨â©Q Z ââ©Q X â¨â©Q (Y â¨â©Q Z)" by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def split_beta' comp_def) lemma qbs_morphism_pair_assoc2: "(λ(x,(y,z)). ((x,y),z)) â X â¨â©Q (Y â¨â©Q Z) ââ©Q (X â¨â©Q Y) â¨â©Q Z" by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def split_beta' comp_def) lemma pair_qbs_fst: assumes "qbs_space Y â {}" shows "map_qbs fst (X â¨â©Q Y) = X" proof(rule qbs_eqI) show "qbs_Mx (map_qbs fst (X â¨â©Q Y)) = qbs_Mx X" proof auto fix αx assume hx:"αx â qbs_Mx X" obtain αy where hy:"αy â qbs_Mx Y" using qbs_empty_equiv[of Y] assms by auto show "âαâpair_qbs_Mx X Y. αx = fst â α" by(auto intro!: exI[where x="λr. (αx r, αy r)"] simp: pair_qbs_Mx_def hx hy comp_def) qed (simp add: pair_qbs_Mx_def) qed lemma pair_qbs_snd: assumes "qbs_space X â {}" shows "map_qbs snd (X â¨â©Q Y) = Y" proof(rule qbs_eqI) show "qbs_Mx (map_qbs snd (X â¨â©Q Y)) = qbs_Mx Y" proof auto fix αy assume hy:"αy â qbs_Mx Y" obtain αx where hx:"αx â qbs_Mx X" using qbs_empty_equiv[of X] assms by auto show "âαâpair_qbs_Mx X Y. αy = snd â α" by(auto intro!: exI[where x="λr. (αx r, αy r)"] simp: pair_qbs_Mx_def hx hy comp_def) qed (simp add: pair_qbs_Mx_def) qed text â¹ The following lemma corresponds to \cite{Heunen_2017} Proposition 19(1). ⺠lemma r_preserves_product : "measure_to_qbs (X â¨â©M Y) = measure_to_qbs X â¨â©Q measure_to_qbs Y" by(auto intro!: qbs_eqI simp: measurable_pair_iff pair_qbs_Mx_def) lemma l_product_sets[simp,measurable_cong]: "sets (qbs_to_measure X â¨â©M qbs_to_measure Y) â sets (qbs_to_measure (X â¨â©Q Y))" proof(rule sets_pair_in_sets,simp) fix A B assume h:"A â sigma_Mx X" "B â sigma_Mx Y" then obtain Ua Ub where hu: "A = Ua â© qbs_space X" "âαâqbs_Mx X. α -` Ua â sets real_borel" "B = Ub â© qbs_space Y" "âαâqbs_Mx Y. α -` Ub â sets real_borel" by(auto simp add: sigma_Mx_def) show "A à B â sigma_Mx (X â¨â©Q Y)" proof(simp add: sigma_Mx_def, rule exI[where x="Ua à Ub"]) show "A à B = Ua à Ub â© qbs_space X à qbs_space Y â§ (âαâpair_qbs_Mx X Y. α -` (Ua à Ub) â sets real_borel)" using hu by(auto simp add: pair_qbs_Mx_def vimage_Times) qed qed lemma(in pair_standard_borel) l_r_r_sets[simp,measurable_cong]: "sets (qbs_to_measure (measure_to_qbs M â¨â©Q measure_to_qbs N)) = sets (M â¨â©M N)" by(simp only: r_preserves_product[symmetric]) (rule standard_borel_lr_sets_ident) end
Theory Product_QuasiBorel
(* Title: Product_QuasiBorel.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) subsubsection â¹ Product Spaces⺠theory Product_QuasiBorel imports "Binary_Product_QuasiBorel" begin definition prod_qbs_Mx :: "['a set, 'a â 'b quasi_borel] â (real â 'a â 'b) set" where "prod_qbs_Mx I M â¡ { α | α. âi. (i â I â¶ (λr. α r i) â qbs_Mx (M i)) â§ (i â I â¶ (λr. α r i) = (λr. undefined))}" lemma prod_qbs_MxI: assumes "âi. i â I â¹ (λr. α r i) â qbs_Mx (M i)" and "âi. i â I â¹ (λr. α r i) = (λr. undefined)" shows "α â prod_qbs_Mx I M" using assms by(auto simp: prod_qbs_Mx_def) lemma prod_qbs_MxE: assumes "α â prod_qbs_Mx I M" shows "âi. i â I â¹ (λr. α r i) â qbs_Mx (M i)" and "âi. i â I â¹ (λr. α r i) = (λr. undefined)" and "âi r. i â I ⹠α r i = undefined" using assms by(auto simp: prod_qbs_Mx_def dest: fun_cong[where g="(λr. undefined)"]) definition PiQ :: "'a set â ('a â 'b quasi_borel) â ('a â 'b) quasi_borel" where "PiQ I M â¡ Abs_quasi_borel (Î â©E iâI. qbs_space (M i), prod_qbs_Mx I M)" syntax "_PiQ" :: "pttrn â 'i set â 'a quasi_borel â ('i => 'a) quasi_borel" ("(3Î â©Q _â_./ _)" 10) translations "Î â©Q xâI. M" == "CONST PiQ I (λx. M)" lemma PiQ_f: "prod_qbs_Mx I M â UNIV â (Î â©E iâI. qbs_space (M i))" using prod_qbs_MxE by fastforce lemma PiQ_closed1: "qbs_closed1 (prod_qbs_Mx I M)" proof(rule qbs_closed1I) fix α f assume h:"α â prod_qbs_Mx I M " "f â real_borel ââ©M real_borel" show "α â f â prod_qbs_Mx I M" proof(rule prod_qbs_MxI) fix i assume "i â I" from prod_qbs_MxE(1)[OF h(1) this] have "(λr. α r i) â f â qbs_Mx (M i)" using h(2) by auto thus "(λr. (α â f) r i) â qbs_Mx (M i)" by(simp add: comp_def) next fix i assume "i â I" from prod_qbs_MxE(3)[OF h(1) this] show "(λr. (α â f) r i) = (λr. undefined)" by simp qed qed lemma PiQ_closed2: "qbs_closed2 (Î â©E iâI. qbs_space (M i)) (prod_qbs_Mx I M)" proof(rule qbs_closed2I) fix x assume h:"x â (Î â©E iâI. qbs_space (M i))" show "(λr. x) â prod_qbs_Mx I M" proof(rule prod_qbs_MxI) fix i assume hi:"i â I" then have "x i â qbs_space (M i)" using h by auto thus "(λr. x i) â qbs_Mx (M i)" by auto next show "âi. i â I â¹ (λr. x i) = (λr. undefined)" using h by auto qed qed lemma PiQ_closed3: "qbs_closed3 (prod_qbs_Mx I M)" proof(rule qbs_closed3I) fix P Fi assume h:"âi::nat. P -` {i} â sets real_borel" "âi::nat. Fi i â prod_qbs_Mx I M" show "(λr. Fi (P r) r) â prod_qbs_Mx I M" proof(rule prod_qbs_MxI) fix i assume hi:"i â I" show "(λr. Fi (P r) r i) â qbs_Mx (M i)" using prod_qbs_MxE(1)[OF h(2) hi] qbs_closed3_dest[OF h(1),of "λj r. Fi j r i"] by auto next show "âi. i â I â¹ (λr. Fi (P r) r i) = (λr. undefined)" using prod_qbs_MxE[OF h(2)] by auto qed qed lemma PiQ_correct: "Rep_quasi_borel (PiQ I M) = (Î â©E iâI. qbs_space (M i), prod_qbs_Mx I M)" by(auto intro!: Abs_quasi_borel_inverse PiQ_f is_quasi_borel_intro simp: PiQ_def PiQ_closed1 PiQ_closed2 PiQ_closed3) lemma PiQ_space[simp]: "qbs_space (PiQ I M) = (Î â©E iâI. qbs_space (M i))" by(simp add: qbs_space_def PiQ_correct) lemma PiQ_Mx[simp]: "qbs_Mx (PiQ I M) = prod_qbs_Mx I M" by(simp add: qbs_Mx_def PiQ_correct) lemma qbs_morphism_component_singleton: assumes "i â I" shows "(λx. x i) â (Î â©Q iâI. (M i)) ââ©Q M i" by(auto intro!: qbs_morphismI simp: prod_qbs_Mx_def comp_def assms) lemma product_qbs_canonical1: assumes "âi. i â I â¹ f i â Y ââ©Q X i" and "âi. i â I â¹ f i = (λy. undefined)" shows "(λy i. f i y) â Y ââ©Q (Î â©Q iâI. X i)" using qbs_morphismE(3)[simplified comp_def,OF assms(1)] assms(2) by(auto intro!: qbs_morphismI prod_qbs_MxI) lemma product_qbs_canonical2: assumes "âi. i â I â¹ f i â Y ââ©Q X i" "âi. i â I â¹ f i = (λy. undefined)" "g â Y ââ©Q (Î â©Q iâI. X i)" "âi. i â I â¹ f i = (λx. x i) â g" and "y â qbs_space Y" shows "g y = (λi. f i y)" proof(rule ext)+ fix i show "g y i = f i y" proof(cases "i â I") case True then show ?thesis using assms(4)[of i] by simp next case False moreover have "(λr. y) â qbs_Mx Y" using assms(5) by simp ultimately show ?thesis using assms(2,3) qbs_morphismE(3)[OF assms(3) _] by(fastforce simp: prod_qbs_Mx_def) qed qed lemma merge_qbs_morphism: "merge I J â (Î â©Q iâI. (M i)) â¨â©Q (Î â©Q jâJ. (M j)) ââ©Q (Î â©Q iâIâªJ. (M i))" proof(rule qbs_morphismI) fix α assume h:"α â qbs_Mx ((Î â©Q iâI. (M i)) â¨â©Q (Î â©Q jâJ. (M j)))" show "merge I J â α â qbs_Mx (Î â©Q iâIâªJ. (M i))" proof(simp, rule prod_qbs_MxI) fix i assume "i â I ⪠J" then consider "i â I" | "i â I â§ i â J" | "i â I â§ i â J" by auto then show "(λr. (merge I J â α) r i) â qbs_Mx (M i)" apply cases using h by(auto simp: merge_def pair_qbs_Mx_def split_beta' dest: prod_qbs_MxE) next fix i assume "i â I ⪠J" then show "(λr. (merge I J â α) r i) = (λr. undefined)" using h by(auto simp: merge_def pair_qbs_Mx_def split_beta' dest: prod_qbs_MxE ) qed qed text â¹ The following lemma corresponds to \cite{Heunen_2017} Proposition 19(1). ⺠lemma r_preserves_product': "measure_to_qbs (Î â©M iâI. M i) = (Î â©Q iâI. measure_to_qbs (M i))" proof(rule qbs_eqI) show "qbs_Mx (measure_to_qbs (Piâ©M I M)) = qbs_Mx (Î â©Q iâI. measure_to_qbs (M i))" proof auto fix f assume h:"f â real_borel ââ©M Piâ©M I M" show "f â prod_qbs_Mx I (λi. measure_to_qbs (M i))" proof(rule prod_qbs_MxI) fix i assume 1:"i â I" show "(λr. f r i) â qbs_Mx (measure_to_qbs (M i))" using measurable_comp[OF h measurable_component_singleton[OF 1,of M]] by (simp add: comp_def) next fix i assume 1:"i â I" then show "(λr. f r i) = (λr. undefined)" using measurable_space[OF h] 1 by(auto simp: space_PiM PiE_def extensional_def) qed next fix f assume h:"f â prod_qbs_Mx I (λi. measure_to_qbs (M i))" show "f â real_borel ââ©M Piâ©M I M" apply(rule measurable_PiM_single') using prod_qbs_MxE(1)[OF h] apply auto[1] using PiQ_f[of I M] h by auto qed qed text â¹ $\prod_{i = 0,1} X_i \cong X_1 \times X_2$. ⺠lemma product_binary_product: "âf g. f â (Î â©Q iâUNIV. if i then X else Y) ââ©Q X â¨â©Q Y â§ g â X â¨â©Q Y ââ©Q (Î â©Q iâUNIV. if i then X else Y) â§ g â f = id â§ f â g = id" by(auto intro!: exI[where x="λf. (f True, f False)"] exI[where x="λxy b. if b then fst xy else snd xy"] qbs_morphismI simp: prod_qbs_Mx_def pair_qbs_Mx_def comp_def all_bool_eq ext) end
>
Theory Binary_CoProduct_QuasiBorel
(* Title: Binary_CoProduct_QuasiBorel.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) subsection â¹Coproduct Spaces⺠theory Binary_CoProduct_QuasiBorel imports "Measure_QuasiBorel_Adjunction" begin subsubsection â¹ Binary Coproduct Spaces ⺠definition copair_qbs_Mx :: "['a quasi_borel, 'b quasi_borel] â (real => 'a + 'b) set" where "copair_qbs_Mx X Y â¡ {g. â S â sets real_borel. (S = {} â¶ (â α1â qbs_Mx X. g = (λr. Inl (α1 r)))) â§ (S = UNIV â¶ (â α2â qbs_Mx Y. g = (λr. Inr (α2 r)))) â§ ((S â {} â§ S â UNIV) â¶ (â α1â qbs_Mx X. â α2â qbs_Mx Y. g = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r)))))}" definition copair_qbs :: "['a quasi_borel, 'b quasi_borel] â ('a + 'b) quasi_borel" (infixr "<+>â©Q" 65) where "copair_qbs X Y â¡ Abs_quasi_borel (qbs_space X <+> qbs_space Y, copair_qbs_Mx X Y)" text â¹ The followin is an equivalent definition of @{term copair_qbs_Mx}. ⺠definition copair_qbs_Mx2 :: "['a quasi_borel, 'b quasi_borel] â (real => 'a + 'b) set" where "copair_qbs_Mx2 X Y â¡ {g. (if qbs_space X = {} â§ qbs_space Y = {} then False else if qbs_space X â {} â§ qbs_space Y = {} then (âα1â qbs_Mx X. g = (λr. Inl (α1 r))) else if qbs_space X = {} â§ qbs_space Y â {} then (âα2â qbs_Mx Y. g = (λr. Inr (α2 r))) else (âS â sets real_borel. âα1â qbs_Mx X. âα2â qbs_Mx Y. g = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r))))) }" lemma copair_qbs_Mx_equiv :"copair_qbs_Mx (X :: 'a quasi_borel) (Y :: 'b quasi_borel) = copair_qbs_Mx2 X Y" proof(auto) (* â *) fix g :: "real â 'a + 'b" assume "g â copair_qbs_Mx X Y" then obtain S where hs:"Sâ sets real_borel â§ (S = {} â¶ (â α1â qbs_Mx X. g = (λr. Inl (α1 r)))) â§ (S = UNIV â¶ (â α2â qbs_Mx Y. g = (λr. Inr (α2 r)))) â§ ((S â {} â§ S â UNIV) â¶ (â α1â qbs_Mx X. â α2â qbs_Mx Y. g = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r)))))" by (auto simp add: copair_qbs_Mx_def) consider "S = {}" | "S = UNIV" | "S â {} â§ S â UNIV" by auto then show "g â copair_qbs_Mx2 X Y" proof cases assume "S = {}" from hs this have "â α1â qbs_Mx X. g = (λr. Inl (α1 r))" by simp then obtain α1 where h1:"α1â qbs_Mx X â§ g = (λr. Inl (α1 r))" by auto have "qbs_space X â {}" using qbs_empty_equiv h1 by auto then have "(qbs_space X â {} â§ qbs_space Y = {}) ⨠(qbs_space X â {} â§ qbs_space Y â {})" by simp then show "g â copair_qbs_Mx2 X Y" proof assume "qbs_space X â {} â§ qbs_space Y = {}" then show "g â copair_qbs_Mx2 X Y" by(simp add: copair_qbs_Mx2_def â¹â α1â qbs_Mx X. g = (λr. Inl (α1 r))âº) next assume "qbs_space X â {} â§ qbs_space Y â {}" then obtain α2 where "α2 â qbs_Mx Y" using qbs_empty_equiv by force define S' :: "real set" where "S' â¡ UNIV" define g' :: "real â 'a + 'b" where "g' â¡ (λr::real. (if (r â S') then Inl (α1 r) else Inr (α2 r)))" from â¹qbs_space X â {} â§ qbs_space Y â {}⺠h1 â¹Î±2 â qbs_Mx Y⺠have "g' â copair_qbs_Mx2 X Y" by(force simp add: S'_def g'_def copair_qbs_Mx2_def) moreover have "g = g'" using h1 by(simp add: g'_def S'_def) ultimately show ?thesis by simp qed next assume "S = UNIV" from hs this have "â α2â qbs_Mx Y. g = (λr. Inr (α2 r))" by simp then obtain α2 where h2:"α2â qbs_Mx Y â§ g = (λr. Inr (α2 r))" by auto have "qbs_space Y â {}" using qbs_empty_equiv h2 by auto then have "(qbs_space X = {} â§ qbs_space Y â {}) ⨠(qbs_space X â {} â§ qbs_space Y â {})" by simp then show "g â copair_qbs_Mx2 X Y" proof assume "qbs_space X = {} â§ qbs_space Y â {}" then show ?thesis by(simp add: copair_qbs_Mx2_def â¹â α2â qbs_Mx Y. g = (λr. Inr (α2 r))âº) next assume "qbs_space X â {} â§ qbs_space Y â {}" then obtain α1 where "α1 â qbs_Mx X" using qbs_empty_equiv by force define S' :: "real set" where "S' â¡ {}" define g' :: "real â 'a + 'b" where "g' â¡ (λr::real. (if (r â S') then Inl (α1 r) else Inr (α2 r)))" from â¹qbs_space X â {} â§ qbs_space Y â {}⺠h2 â¹Î±1 â qbs_Mx X⺠have "g' â copair_qbs_Mx2 X Y" by(force simp add: S'_def g'_def copair_qbs_Mx2_def) moreover have "g = g'" using h2 by(simp add: g'_def S'_def) ultimately show ?thesis by simp qed next assume "S â {} â§ S â UNIV" then have h: "â α1â qbs_Mx X. â α2â qbs_Mx Y. g = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r)))" using hs by simp then have "qbs_space X â {} â§ qbs_space Y â {}" by (metis empty_iff qbs_empty_equiv) thus ?thesis using hs h by(auto simp add: copair_qbs_Mx2_def) qed (* â *) next fix g :: "real â 'a + 'b" assume "g â copair_qbs_Mx2 X Y" then have h: "if qbs_space X = {} â§ qbs_space Y = {} then False else if qbs_space X â {} â§ qbs_space Y = {} then (âα1â qbs_Mx X. g = (λr. Inl (α1 r))) else if qbs_space X = {} â§ qbs_space Y â {} then (âα2â qbs_Mx Y. g = (λr. Inr (α2 r))) else (âS â sets real_borel. âα1â qbs_Mx X. âα2â qbs_Mx Y. g = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r))))" by(simp add: copair_qbs_Mx2_def) consider "(qbs_space X = {} â§ qbs_space Y = {})" | "(qbs_space X â {} â§ qbs_space Y = {})" | "(qbs_space X = {} â§ qbs_space Y â {})" | "(qbs_space X â {} â§ qbs_space Y â {})" by auto then show "g â copair_qbs_Mx X Y" proof cases assume "qbs_space X = {} â§ qbs_space Y = {}" then show ?thesis using â¹g â copair_qbs_Mx2 X Y⺠by(simp add: copair_qbs_Mx2_def) next assume "qbs_space X â {} â§ qbs_space Y = {}" from h this have "âα1â qbs_Mx X. g = (λr. Inl (α1 r))" by simp thus ?thesis by(auto simp add: copair_qbs_Mx_def) next assume "qbs_space X = {} â§ qbs_space Y â {}" from h this have "âα2â qbs_Mx Y. g = (λr. Inr (α2 r))" by simp thus ?thesis unfolding copair_qbs_Mx_def by(force simp add: copair_qbs_Mx_def) next assume "qbs_space X â {} â§ qbs_space Y â {}" from h this have "âS â sets real_borel. âα1â qbs_Mx X. âα2â qbs_Mx Y. g = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r)))" by simp then show ?thesis proof(auto simp add: exE) fix S fix α1 fix α2 assume "S â sets real_borel" "α1 â qbs_Mx X" "α2 â qbs_Mx Y" "g = (λr. if r â S then Inl (α1 r) else Inr (α2 r))" consider "S = {}" | "S = UNIV" | "S â {} â§ S â UNIV" by auto then show "(λr. if r â S then Inl (α1 r) else Inr (α2 r)) â copair_qbs_Mx X Y" proof cases assume "S = {}" then have [simp]: "(λr. if r â S then Inl (α1 r) else Inr (α2 r)) = (λr. Inr (α2 r))" by simp have "UNIV â sets real_borel" by simp then show ?thesis using â¹Î±2 â qbs_Mx Y⺠unfolding copair_qbs_Mx_def by(auto intro! : bexI[where x=UNIV]) next assume "S = UNIV" then have "(λr. if r â S then Inl (α1 r) else Inr (α2 r)) = (λr. Inl (α1 r))" by simp then show ?thesis using â¹Î±1 â qbs_Mx X⺠by(auto simp add: copair_qbs_Mx_def) next assume "S â {} â§ S â UNIV" then show ?thesis using â¹S â sets real_borel⺠â¹Î±1 â qbs_Mx X⺠â¹Î±2 â qbs_Mx Y⺠by(auto simp add: copair_qbs_Mx_def) qed qed qed qed lemma copair_qbs_f[simp]: "copair_qbs_Mx X Y â UNIV â qbs_space X <+> qbs_space Y" proof fix g assume "g â copair_qbs_Mx X Y" then obtain S where hs:"Sâ sets real_borel â§ (S = {} â¶ (â α1â qbs_Mx X. g = (λr. Inl (α1 r)))) â§ (S = UNIV â¶ (â α2â qbs_Mx Y. g = (λr. Inr (α2 r)))) â§ ((S â {} â§ S â UNIV) â¶ (â α1â qbs_Mx X. â α2â qbs_Mx Y. g = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r)))))" by (auto simp add: copair_qbs_Mx_def) consider "S = {}" | "S = UNIV" | "S â {} â§ S â UNIV" by auto then show "g â UNIV â qbs_space X <+> qbs_space Y" proof cases assume "S = {}" then show ?thesis using hs by auto next assume "S = UNIV" then show ?thesis using hs by auto next assume "S â {} â§ S â UNIV" then have "â α1â qbs_Mx X. â α2â qbs_Mx Y. g = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r)))" using hs by simp then show ?thesis by(auto simp add: exE) qed qed lemma copair_qbs_closed1: "qbs_closed1 (copair_qbs_Mx X Y)" proof(auto simp add: qbs_closed1_def) fix g fix f assume "g â copair_qbs_Mx X Y" "f â real_borel ââ©M real_borel" then have "g â copair_qbs_Mx2 X Y" using copair_qbs_Mx_equiv by auto consider "(qbs_space X = {} â§ qbs_space Y = {})" | "(qbs_space X â {} â§ qbs_space Y = {})" | "(qbs_space X = {} â§ qbs_space Y â {})" | "(qbs_space X â {} â§ qbs_space Y â {})" by auto then have "g â f â copair_qbs_Mx2 X Y" proof cases assume "qbs_space X = {} â§ qbs_space Y = {}" then show ?thesis using â¹g â copair_qbs_Mx2 X Y⺠qbs_empty_equiv by(simp add: copair_qbs_Mx2_def) next assume "qbs_space X â {} â§ qbs_space Y = {}" then obtain α1 where h1:"α1â qbs_Mx X â§ g = (λr. Inl (α1 r))" using â¹g â copair_qbs_Mx2 X Y⺠by(auto simp add: copair_qbs_Mx2_def) then have "α1 â f â qbs_Mx X" using â¹f â real_borel ââ©M real_borel⺠by auto moreover have "g â f = (λr. Inl ((α1 â f) r))" using h1 by auto ultimately show ?thesis using â¹qbs_space X â {} â§ qbs_space Y = {}⺠by(force simp add: copair_qbs_Mx2_def) next assume "(qbs_space X = {} â§ qbs_space Y â {})" then obtain α2 where h2:"α2â qbs_Mx Y â§ g = (λr. Inr (α2 r))" using â¹g â copair_qbs_Mx2 X Y⺠by(auto simp add: copair_qbs_Mx2_def) then have "α2 â f â qbs_Mx Y" using â¹f â real_borel ââ©M real_borel⺠by auto moreover have "g â f = (λr. Inr ((α2 â f) r))" using h2 by auto ultimately show ?thesis using â¹(qbs_space X = {} â§ qbs_space Y â {})⺠by(force simp add: copair_qbs_Mx2_def) next assume "qbs_space X â {} â§ qbs_space Y â {}" then have "âS â sets real_borel. âα1â qbs_Mx X. âα2â qbs_Mx Y. g = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r)))" using â¹g â copair_qbs_Mx2 X Y⺠by(simp add: copair_qbs_Mx2_def) then show ?thesis proof(auto simp add: exE) fix S fix α1 fix α2 assume "S â sets real_borel" "α1â qbs_Mx X" "α2 â qbs_Mx Y" "g = (λr. if r â S then Inl (α1 r) else Inr (α2 r))" have "f -` S â sets real_borel" using â¹f â real_borel ââ©M real_borel⺠â¹S â sets real_borel⺠by (simp add: measurable_sets_borel) moreover have "α1 â f â qbs_Mx X" using â¹Î±1â qbs_Mx X⺠â¹f â real_borel ââ©M real_borel⺠qbs_decomp by(auto simp add: qbs_closed1_def) moreover have "α2 â f â qbs_Mx Y" using â¹Î±2â qbs_Mx Y⺠â¹f â real_borel ââ©M real_borel⺠qbs_decomp by(auto simp add: qbs_closed1_def) moreover have "(λr. if r â S then Inl (α1 r) else Inr (α2 r)) â f = (λr. if r â f -` S then Inl ((α1 â f) r) else Inr ((α2 â f) r))" by auto ultimately show "(λr. if r â S then Inl (α1 r) else Inr (α2 r)) â f â copair_qbs_Mx2 X Y" using â¹qbs_space X â {} â§ qbs_space Y â {}⺠by(force simp add: copair_qbs_Mx2_def) qed qed thus "g â f â copair_qbs_Mx X Y" using copair_qbs_Mx_equiv by auto qed lemma copair_qbs_closed2: "qbs_closed2 (qbs_space X <+> qbs_space Y) (copair_qbs_Mx X Y)" proof(auto simp add: qbs_closed2_def) fix x assume "x â qbs_space X" define α1 :: "real â _" where "α1 â¡ (λr. x)" have "α1 â qbs_Mx X" using â¹x â qbs_space X⺠qbs_decomp by(force simp add: qbs_closed2_def α1_def ) moreover have "(λr. Inl x) = (λl. Inl (α1 l))" by (simp add: α1_def) moreover have "{} â sets real_borel" by auto ultimately show "(λr. Inl x) â copair_qbs_Mx X Y" by(auto simp add: copair_qbs_Mx_def) next fix y assume "y â qbs_space Y" define α2 :: "real â _" where "α2 â¡ (λr. y)" have "α2 â qbs_Mx Y" using â¹y â qbs_space Y⺠qbs_decomp by(force simp add: qbs_closed2_def α2_def ) moreover have "(λr. Inr y) = (λl. Inr (α2 l))" by (simp add: α2_def) moreover have "UNIV â sets real_borel" by auto ultimately show "(λr. Inr y) â copair_qbs_Mx X Y" unfolding copair_qbs_Mx_def by(auto intro!: bexI[where x=UNIV]) qed lemma copair_qbs_closed3: "qbs_closed3 (copair_qbs_Mx X Y)" proof(auto simp add: qbs_closed3_def) fix P :: "real â nat" fix Fi :: "nat â real â_ + _" assume "âi. P -` {i} â sets real_borel" "âi. Fi i â copair_qbs_Mx X Y" then have "âi. Fi i â copair_qbs_Mx2 X Y" using copair_qbs_Mx_equiv by blast consider "(qbs_space X = {} â§ qbs_space Y = {})" | "(qbs_space X â {} â§ qbs_space Y = {})" | "(qbs_space X = {} â§ qbs_space Y â {})" | "(qbs_space X â {} â§ qbs_space Y â {})" by auto then have "(λr. Fi (P r) r) â copair_qbs_Mx2 X Y" proof cases assume "qbs_space X = {} â§ qbs_space Y = {}" then show ?thesis using â¹âi. Fi i â copair_qbs_Mx2 X Y⺠qbs_empty_equiv by(simp add: copair_qbs_Mx2_def) next assume "qbs_space X â {} â§ qbs_space Y = {}" then have "âi. âαi. αi â qbs_Mx X â§ Fi i = (λr. Inl (αi r))" using â¹âi. Fi i â copair_qbs_Mx2 X Y⺠by(auto simp add: copair_qbs_Mx2_def) then have "âα1. âi. α1 i â qbs_Mx X â§ Fi i = (λr. Inl (α1 i r))" by(rule choice) then obtain α1 :: "nat â real â _" where h1: "âi. α1 i â qbs_Mx X â§ Fi i = (λr. Inl (α1 i r))" by auto define β :: "real â _" where "β â¡ (λr. α1 (P r) r)" from â¹âi. P -` {i} â sets real_borel⺠h1 have "β â qbs_Mx X" by (simp add: β_def) moreover have "(λr. Fi (P r) r) = (λr. Inl (β r))" using h1 by(simp add: β_def) ultimately show ?thesis using â¹qbs_space X â {} â§ qbs_space Y = {}⺠by (auto simp add: copair_qbs_Mx2_def) next assume "qbs_space X = {} â§ qbs_space Y â {}" then have "âi. âαi. αi â qbs_Mx Y â§ Fi i = (λr. Inr (αi r))" using â¹âi. Fi i â copair_qbs_Mx2 X Y⺠by(auto simp add: copair_qbs_Mx2_def) then have "âα2. âi. α2 i â qbs_Mx Y â§ Fi i = (λr. Inr (α2 i r))" by(rule choice) then obtain α2 :: "nat â real â _" where h2: "âi. α2 i â qbs_Mx Y â§ Fi i = (λr. Inr (α2 i r))" by auto define β :: "real â _" where "β â¡ (λr. α2 (P r) r)" from â¹âi. P -` {i} â sets real_borel⺠h2 qbs_decomp have "β â qbs_Mx Y" by(simp add: β_def) moreover have "(λr. Fi (P r) r) = (λr. Inr (β r))" using h2 by(simp add: β_def) ultimately show ?thesis using â¹qbs_space X = {} â§ qbs_space Y â {}⺠by (auto simp add: copair_qbs_Mx2_def) next assume "qbs_space X â {} â§ qbs_space Y â {}" then have "âi. âSi. Si â sets real_borel â§ (âα1iâ qbs_Mx X. âα2iâ qbs_Mx Y. Fi i = (λr::real. (if (r â Si) then Inl (α1i r) else Inr (α2i r))))" using â¹âi. Fi i â copair_qbs_Mx2 X Y⺠by (auto simp add: copair_qbs_Mx2_def) then have "âS. âi. S i â sets real_borel â§ (âα1iâ qbs_Mx X. âα2iâ qbs_Mx Y. Fi i = (λr::real. (if (r â S i) then Inl (α1i r) else Inr (α2i r))))" by(rule choice) then obtain S :: "nat â real set" where hs :"âi. S i â sets real_borel â§ (âα1iâ qbs_Mx X. âα2iâ qbs_Mx Y. Fi i = (λr::real. (if (r â S i) then Inl (α1i r) else Inr (α2i r))))" by auto then have "âi. âα1i. α1i â qbs_Mx X â§ (âα2iâ qbs_Mx Y. Fi i = (λr::real. (if (r â S i) then Inl (α1i r) else Inr (α2i r))))" by blast then have "âα1. âi. α1 i â qbs_Mx X â§ (âα2iâ qbs_Mx Y. Fi i = (λr::real. (if (r â S i) then Inl (α1 i r) else Inr (α2i r))))" by(rule choice) then obtain α1 where h1: "âi. α1 i â qbs_Mx X â§ (âα2iâ qbs_Mx Y. Fi i = (λr::real. (if (r â S i) then Inl (α1 i r) else Inr (α2i r))))" by auto define β1 :: "real â _" where "β1 â¡ (λr. α1 (P r) r)" from â¹âi. P -` {i} â sets real_borel⺠h1 qbs_decomp have "β1 â qbs_Mx X" by(simp add: β1_def) from h1 have "âi. âα2i. α2iâ qbs_Mx Y â§ Fi i = (λr::real. (if (r â S i) then Inl (α1 i r) else Inr (α2i r)))" by auto then have "âα2. âi. α2 iâ qbs_Mx Y â§ Fi i = (λr::real. (if (r â S i) then Inl (α1 i r) else Inr (α2 i r)))" by(rule choice) then obtain α2 where h2: "âi. α2 iâ qbs_Mx Y â§ Fi i = (λr::real. (if (r â S i) then Inl (α1 i r) else Inr (α2 i r)))" by auto define β2 :: "real â _" where "β2 â¡ (λr. α2 (P r) r)" from â¹âi. P -` {i} â sets real_borel⺠h2 qbs_decomp have "β2 â qbs_Mx Y" by(simp add: β2_def) define A :: "nat â real set" where "A â¡ (λi. S i â© P -` {i})" have "âi. A i â sets real_borel" using A_def â¹âi. P -` {i} â sets real_borel⺠hs by blast define S' :: "real set" where "S' â¡ {r. r â S (P r)}" have "S' = (âi::nat. A i)" by(auto simp add: S'_def A_def) hence "S' â sets real_borel" using â¹âi. A i â sets real_borel⺠by auto from h2 have "(λr. Fi (P r) r) = (λr. (if r â S' then Inl (β1 r) else Inr (β2 r)))" by(auto simp add: β1_def β2_def S'_def) thus "(λr. Fi (P r) r) â copair_qbs_Mx2 X Y" using â¹qbs_space X â {} â§ qbs_space Y â {}⺠â¹S' â sets real_borel⺠â¹Î²1 â qbs_Mx X⺠â¹Î²2 â qbs_Mx Y⺠by(auto simp add: copair_qbs_Mx2_def) qed thus "(λr. Fi (P r) r) â copair_qbs_Mx X Y" using copair_qbs_Mx_equiv by auto qed lemma copair_qbs_correct: "Rep_quasi_borel (copair_qbs X Y) = (qbs_space X <+> qbs_space Y, copair_qbs_Mx X Y)" unfolding copair_qbs_def by(auto intro!: Abs_quasi_borel_inverse copair_qbs_f simp: copair_qbs_closed2 copair_qbs_closed1 copair_qbs_closed3) lemma copair_qbs_space[simp]: "qbs_space (copair_qbs X Y) = qbs_space X <+> qbs_space Y" by(simp add: qbs_space_def copair_qbs_correct) lemma copair_qbs_Mx[simp]: "qbs_Mx (copair_qbs X Y) = copair_qbs_Mx X Y" by(simp add: qbs_Mx_def copair_qbs_correct) lemma Inl_qbs_morphism: "Inl â X ââ©Q X <+>â©Q Y" proof(rule qbs_morphismI) fix α assume "α â qbs_Mx X" moreover have "Inl â α = (λr. Inl (α r))" by auto ultimately show "Inl â α â qbs_Mx (X <+>â©Q Y)" by(auto simp add: copair_qbs_Mx_def) qed lemma Inr_qbs_morphism: "Inr â Y ââ©Q X <+>â©Q Y" proof(rule qbs_morphismI) fix α assume "α â qbs_Mx Y" moreover have "Inr â α = (λr. Inr (α r))" by auto ultimately show "Inr â α â qbs_Mx (X <+>â©Q Y)" by(auto intro!: bexI[where x=UNIV] simp add: copair_qbs_Mx_def) qed lemma case_sum_preserves_morphisms: assumes "f â X ââ©Q Z" and "g â Y ââ©Q Z" shows "case_sum f g â X <+>â©Q Y ââ©Q Z" proof(rule qbs_morphismI;auto) fix α assume "α â copair_qbs_Mx X Y" then obtain S where hs:"Sâ sets real_borel â§ (S = {} â¶ (â α1â qbs_Mx X. α = (λr. Inl (α1 r)))) â§ (S = UNIV â¶ (â α2â qbs_Mx Y. α = (λr. Inr (α2 r)))) â§ ((S â {} â§ S â UNIV) â¶ (â α1â qbs_Mx X. â α2â qbs_Mx Y. α = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r)))))" by (auto simp add: copair_qbs_Mx_def) consider "S = {}" | "S = UNIV" | "S â {} â§ S â UNIV" by auto then show "case_sum f g â α â qbs_Mx Z" proof cases assume "S = {}" then obtain α1 where h1: "α1â qbs_Mx X ⧠α = (λr. Inl (α1 r))" using hs by auto then have "f â α1 â qbs_Mx Z" using assms by(auto simp add: qbs_morphism_def) moreover have "case_sum f g â α = f â α1" using h1 by auto ultimately show ?thesis by simp next assume "S = UNIV" then obtain α2 where h2: "α2â qbs_Mx Y ⧠α = (λr. Inr (α2 r))" using hs by auto then have "g â α2 â qbs_Mx Z" using assms by(auto simp add: qbs_morphism_def) moreover have "case_sum f g â α = g â α2" using h2 by auto ultimately show ?thesis by simp next assume "S â {} â§ S â UNIV" then obtain α1 α2 where h: "α1â qbs_Mx X ⧠α2â qbs_Mx Y ⧠α = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r)))" using hs by auto define F :: "nat â real â _" where "F â¡ (λi r. (if i = 0 then (f â α1) r else (g â α2) r))" define P :: "real â nat" where "P â¡ (λr. if r â S then 0 else 1)" have "f â α1 â qbs_Mx Z" using assms h by(simp add: qbs_morphism_def) have "g â α2 â qbs_Mx Z" using assms h by(simp add: qbs_morphism_def) have "âi. F i â qbs_Mx Z" proof(auto simp add: F_def) fix i :: nat consider "i = 0" | "i â 0" by auto then show "(λr. if i = 0 then (f â α1) r else (g â α2) r) â qbs_Mx Z" proof cases assume "i = 0" then have "(λr. if i = 0 then (f â α1) r else (g â α2) r) = f â α1" by auto then show ?thesis using â¹f â α1 â qbs_Mx Z⺠by simp next assume "i â 0" then have "(λr. if i = 0 then (f â α1) r else (g â α2) r) = g â α2" by auto then show ?thesis using â¹g â α2 â qbs_Mx Z⺠by simp qed qed moreover have "âi. P -`{i} â sets real_borel" proof fix i :: nat consider "i = 0" | "i = 1" | "i â 0 â§ i â 1" by auto then show "P -`{i} â sets real_borel" proof cases assume "i = 0" then show ?thesis using hs by(simp add: P_def) next assume "i = 1" then show ?thesis using hs by (simp add: P_def borel_comp) next assume "i â 0 â§ i â 1" then show ?thesis by(simp add: P_def) qed qed ultimately have "(λr. F (P r) r) â qbs_Mx Z" by simp moreover have "case_sum f g â α = (λr. F (P r) r)" using h by(auto simp add: F_def P_def) ultimately show "case_sum f g â α â qbs_Mx Z" by simp qed qed lemma map_sum_preserves_morphisms: assumes "f â X ââ©Q Y" and "g â X' ââ©Q Y'" shows "map_sum f g â X <+>â©Q X' ââ©Q Y <+>â©Q Y'" proof(rule qbs_morphismI,simp) fix α assume "α â copair_qbs_Mx X X'" then obtain S where hs:"Sâ sets real_borel â§ (S = {} â¶ (â α1â qbs_Mx X. α = (λr. Inl (α1 r)))) â§ (S = UNIV â¶ (â α2â qbs_Mx X'. α = (λr. Inr (α2 r)))) â§ ((S â {} â§ S â UNIV) â¶ (â α1â qbs_Mx X. â α2â qbs_Mx X'. α = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r)))))" by (auto simp add: copair_qbs_Mx_def) consider "S = {}" | "S = UNIV" | "S â {} â§ S â UNIV" by auto then show "map_sum f g â α â copair_qbs_Mx Y Y'" proof cases assume "S = {}" then obtain α1 where h1: "α1â qbs_Mx X ⧠α = (λr. Inl (α1 r))" using hs by auto define f' :: "real â _" where "f' â¡ f â α1" then have "f' â qbs_Mx Y" using assms h1 by(simp add: qbs_morphism_def) moreover have "map_sum f g â α = (λr. Inl (f' r))" using h1 by (auto simp add: f'_def) moreover have "{} â sets real_borel" by simp ultimately show ?thesis by(auto simp add: copair_qbs_Mx_def) next assume "S = UNIV" then obtain α2 where h2: "α2â qbs_Mx X' ⧠α = (λr. Inr (α2 r))" using hs by auto define g' :: "real â _" where "g' â¡ g â α2" then have "g' â qbs_Mx Y'" using assms h2 by(simp add: qbs_morphism_def) moreover have "map_sum f g â α = (λr. Inr (g' r))" using h2 by (auto simp add: g'_def) ultimately show ?thesis by(auto intro!: bexI[where x=UNIV] simp add: copair_qbs_Mx_def) next assume "S â {} â§ S â UNIV" then obtain α1 α2 where h: "α1â qbs_Mx X ⧠α2â qbs_Mx X' ⧠α = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r)))" using hs by auto define f' :: "real â _" where "f' â¡ f â α1" define g' :: "real â _" where "g' â¡ g â α2" have "f' â qbs_Mx Y" using assms h by(auto simp: f'_def) moreover have "g' â qbs_Mx Y'" using assms h by(auto simp: g'_def) moreover have "map_sum f g â α = (λr::real. (if (r â S) then Inl (f' r) else Inr (g' r)))" using h by(auto simp add: f'_def g'_def) moreover have "S â sets real_borel" using hs by simp ultimately show ?thesis using â¹S â {} â§ S â UNIV⺠by(auto simp add: copair_qbs_Mx_def) qed qed end
d>
Theory CoProduct_QuasiBorel
(* Title: CoProduct_QuasiBorel.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) subsubsection â¹ Countable Coproduct Spaces ⺠theory CoProduct_QuasiBorel imports "Product_QuasiBorel" "Binary_CoProduct_QuasiBorel" begin definition coprod_qbs_Mx :: "['a set, 'a â 'b quasi_borel] â (real â 'a à 'b) set" where "coprod_qbs_Mx I X â¡ { λr. (f r, α (f r) r) |f α. f â real_borel ââ©M count_space I â§ (âiârange f. α i â qbs_Mx (X i))}" lemma coprod_qbs_MxI: assumes "f â real_borel ââ©M count_space I" and "âi. i â range f ⹠α i â qbs_Mx (X i)" shows "(λr. (f r, α (f r) r)) â coprod_qbs_Mx I X" using assms unfolding coprod_qbs_Mx_def by blast definition coprod_qbs_Mx' :: "['a set, 'a â 'b quasi_borel] â (real â 'a à 'b) set" where "coprod_qbs_Mx' I X â¡ { λr. (f r, α (f r) r) |f α. f â real_borel ââ©M count_space I â§ (âi. (i â range f ⨠qbs_space (X i) â {}) ⶠα i â qbs_Mx (X i))}" lemma coproduct_qbs_Mx_eq: "coprod_qbs_Mx I X = coprod_qbs_Mx' I X" proof auto fix α assume "α â coprod_qbs_Mx I X" then obtain f β where hfb: "f â real_borel ââ©M count_space I" "âi. i â range f ⹠β i â qbs_Mx (X i)" "α = (λr. (f r, β (f r) r))" unfolding coprod_qbs_Mx_def by blast define β' where "β' â¡ (λi. if i â range f then β i else if qbs_space (X i) â {} then (SOME γ. γ â qbs_Mx (X i)) else β i)" have 1:"α = (λr. (f r, β' (f r) r))" by(simp add: hfb(3) β'_def) have 2:"âi. qbs_space (X i) â {} ⹠β' i â qbs_Mx (X i)" proof - fix i assume hne:"qbs_space (X i) â {}" then obtain x where "x â qbs_space (X i)" by auto hence "(λr. x) â qbs_Mx (X i)" by auto thus "β' i â qbs_Mx (X i)" by(cases "i â range f") (auto simp: β'_def hfb(2) hne intro!: someI2[where a="λr. x"]) qed show "α â coprod_qbs_Mx' I X" using hfb(1,2) 1 2 by(auto simp: coprod_qbs_Mx'_def intro!: exI[where x=f] exI[where x=β']) next fix α assume "α â coprod_qbs_Mx' I X" then obtain f β where hfb: "f â real_borel ââ©M count_space I" "âi. qbs_space (X i) â {} ⹠β i â qbs_Mx (X i)" "âi. i â range f ⹠β i â qbs_Mx (X i)" "α = (λr. (f r, β (f r) r))" unfolding coprod_qbs_Mx'_def by blast show "α â coprod_qbs_Mx I X" by(auto simp: hfb(4) intro!: coprod_qbs_MxI[OF hfb(1) hfb(3)]) qed definition coprod_qbs :: "['a set, 'a â 'b quasi_borel] â ('a à 'b) quasi_borel" where "coprod_qbs I X â¡ Abs_quasi_borel (SIGMA i:I. qbs_space (X i), coprod_qbs_Mx I X)" syntax "_coprod_qbs" :: "pttrn â 'i set â 'a quasi_borel â ('i à 'a) quasi_borel" ("(3⨿â©Q _â_./ _)" 10) translations "⨿â©Q xâI. M" â "CONST coprod_qbs I (λx. M)" lemma coprod_qbs_f[simp]: "coprod_qbs_Mx I X â UNIV â (SIGMA i:I. qbs_space (X i))" by(fastforce simp: coprod_qbs_Mx_def dest: measurable_space) lemma coprod_qbs_closed1: "qbs_closed1 (coprod_qbs_Mx I X)" proof(rule qbs_closed1I) fix α f assume "α â coprod_qbs_Mx I X" and 1[measurable]: "f â real_borel ââ©M real_borel" then obtain β g where ha: "âi. i â range g ⹠β i â qbs_Mx (X i)" "α = (λr. (g r, β (g r) r))" and [measurable]:"g â real_borel ââ©M count_space I" by(fastforce simp: coprod_qbs_Mx_def) then have "âi. i â range g ⹠β i â f â qbs_Mx (X i)" by simp thus "α â f â coprod_qbs_Mx I X" by(auto intro!: coprod_qbs_MxI[where f="g â f" and α="λi. β i â f",simplified comp_def] simp: ha(2) comp_def) qed lemma coprod_qbs_closed2: "qbs_closed2 (SIGMA i:I. qbs_space (X i)) (coprod_qbs_Mx I X)" proof(rule qbs_closed2I,auto) fix i x assume "i â I" "x â qbs_space (X i)" then show "(λr. (i,x)) â coprod_qbs_Mx I X" by(auto simp: coprod_qbs_Mx_def intro!: exI[where x="λr. i"]) qed lemma coprod_qbs_closed3: "qbs_closed3 (coprod_qbs_Mx I X)" proof(rule qbs_closed3I) fix P Fi assume h:"âi :: nat. P -` {i} â sets real_borel" "âi :: nat. Fi i â coprod_qbs_Mx I X" then have "âi. âfi αi. Fi i = (λr. (fi r, αi (fi r) r)) â§ fi â real_borel ââ©M count_space I â§ (âj. (j â range fi ⨠qbs_space (X j) â {}) ⶠαi j â qbs_Mx (X j))" by(auto simp: coproduct_qbs_Mx_eq coprod_qbs_Mx'_def) then obtain fi where "âi. âαi. Fi i = (λr. (fi i r, αi (fi i r) r)) â§ fi i â real_borel ââ©M count_space I â§ (âj. (j â range (fi i) ⨠qbs_space (X j) â {}) ⶠαi j â qbs_Mx (X j))" by(fastforce intro!: choice) then obtain αi where "âi. Fi i = (λr. (fi i r, αi i (fi i r) r)) â§ fi i â real_borel ââ©M count_space I â§ (âj. (j â range (fi i) ⨠qbs_space (X j) â {}) ⶠαi i j â qbs_Mx (X j))" by(fastforce intro!: choice) then have hf: "âi. Fi i = (λr. (fi i r, αi i (fi i r) r))" "âi. fi i â real_borel ââ©M count_space I" "âi j. j â range (fi i) ⹠αi i j â qbs_Mx (X j)" "âi j. qbs_space (X j) â {} ⹠αi i j â qbs_Mx (X j)" by auto define f' where "f' â¡ (λr. fi (P r) r)" define α' where "α' â¡ (λi r. αi (P r) i r)" have 1:"(λr. Fi (P r) r) = (λr. (f' r, α' (f' r) r))" by(simp add: α'_def f'_def hf) have "f' â real_borel ââ©M count_space I" proof - note [measurable] = separate_measurable[OF h(1)] have "(λ(n,r). fi n r) â count_space UNIV â¨â©M real_borel ââ©M count_space I" by(auto intro!: measurable_pair_measure_countable1 simp: hf) hence [measurable]:"(λ(n,r). fi n r) â nat_borel â¨â©M real_borel ââ©M count_space I" using measurable_cong_sets[OF sets_pair_measure_cong[OF sets_borel_eq_count_space],of real_borel real_borel] by auto thus ?thesis using measurable_comp[of "λr. (P r, r)" _ _ "(λ(n,r). fi n r)"] by(simp add: f'_def) qed moreover have "âi. i â range f' ⹠α' i â qbs_Mx (X i)" proof - fix i assume hi:"i â range f'" then obtain r where hr: "i = fi (P r) r" by(auto simp: f'_def) hence "i â range (fi (P r))" by simp hence "αi (P r) i â qbs_Mx (X i)" by(simp add: hf) hence "qbs_space (X i) â {}" by(auto simp: qbs_empty_equiv) hence "âj. αi j i â qbs_Mx (X i)" by(simp add: hf(4)) then show "α' i â qbs_Mx (X i)" by(auto simp: α'_def h(1) intro!: qbs_closed3_dest[of P "λj. αi j i"]) qed ultimately show "(λr. Fi (P r) r) â coprod_qbs_Mx I X" by(auto intro!: coprod_qbs_MxI simp: 1) qed lemma coprod_qbs_correct: "Rep_quasi_borel (coprod_qbs I X) = (SIGMA i:I. qbs_space (X i), coprod_qbs_Mx I X)" unfolding coprod_qbs_def using is_quasi_borel_intro[OF coprod_qbs_f coprod_qbs_closed1 coprod_qbs_closed2 coprod_qbs_closed3] by(fastforce intro!: Abs_quasi_borel_inverse) lemma coproduct_qbs_space[simp]: "qbs_space (coprod_qbs I X) = (SIGMA i:I. qbs_space (X i))" by(simp add: coprod_qbs_correct qbs_space_def) lemma coproduct_qbs_Mx[simp]: "qbs_Mx (coprod_qbs I X) = coprod_qbs_Mx I X" by(simp add: coprod_qbs_correct qbs_Mx_def) lemma ini_morphism: assumes "j â I" shows "(λx. (j,x)) â X j ââ©Q (⨿â©Q iâI. X i)" by(fastforce intro!: qbs_morphismI exI[where x="λr. j"] simp: coprod_qbs_Mx_def comp_def assms) lemma coprod_qbs_canonical1: assumes "countable I" and "âi. i â I â¹ f i â X i ââ©Q Y" shows "(λ(i,x). f i x) â (⨿â©Q i âI. X i) ââ©Q Y" proof(rule qbs_morphismI) fix α assume "α â qbs_Mx (coprod_qbs I X)" then obtain β g where ha: "âi. i â range g ⹠β i â qbs_Mx (X i)" "α = (λr. (g r, β (g r) r))" and hg[measurable]:"g â real_borel ââ©M count_space I" by(fastforce simp: coprod_qbs_Mx_def) define f' where "f' â¡ (λi r. f i (β i r))" have "range g â I" using measurable_space[OF hg] by auto hence 1:"(âi. i â range g â¹ f' i â qbs_Mx Y)" using qbs_morphismE(3)[OF assms(2) ha(1),simplified comp_def] by(auto simp: f'_def) have "(λ(i, x). f i x) â α = (λr. f' (g r) r)" by(auto simp: ha(2) f'_def) also have "... â qbs_Mx Y" by(auto intro!: qbs_closed3_dest2'[OF assms(1) hg,of f',OF 1]) finally show "(λ(i, x). f i x) â α â qbs_Mx Y " . qed lemma coprod_qbs_canonical1': assumes "countable I" and "âi. i â I â¹ (λx. f (i,x)) â X i ââ©Q Y" shows "f â (⨿â©Q i âI. X i) ââ©Q Y" using coprod_qbs_canonical1[where f="curry f"] assms by(auto simp: curry_def) text â¹ $\coprod_{i=0,1} X_i \cong X_1 + X_2$. ⺠lemma coproduct_binary_coproduct: "âf g. f â (⨿â©Q iâUNIV. if i then X else Y) ââ©Q X <+>â©Q Y â§ g â X <+>â©Q Y ââ©Q (⨿â©Q iâUNIV. if i then X else Y) â§ g â f = id â§ f â g = id" proof(auto intro!: exI[where x="λ(b,z). if b then Inl z else Inr z"] exI[where x="case_sum (λz. (True,z)) (λz. (False,z))"]) show "(λ(b, z). if b then Inl z else Inr z) â (⨿â©Q iâUNIV. if i then X else Y) ââ©Q X <+>â©Q Y" proof(rule qbs_morphismI) fix α assume " α â qbs_Mx (⨿â©Q iâUNIV. if i then X else Y)" then obtain f β where hf: "α = (λr. (f r, β (f r) r))" "f â real_borel ââ©M count_space UNIV" "âi. i â range f ⹠β i â qbs_Mx (if i then X else Y)" by(auto simp: coprod_qbs_Mx_def) consider "range f = {True}" | "range f = {False}" | "range f = {True,False}" by auto thus "(λ(b, z). if b then Inl z else Inr z) â α â qbs_Mx (X <+>â©Q Y)" proof cases case 1 then have "âr. f r = True" by auto then show ?thesis using hf(3) by(auto intro!: bexI[where x="{}"] bexI[where x="β True"] simp: copair_qbs_Mx_def split_beta' comp_def hf(1)) next case 2 then have "âr. f r = False" by auto then show ?thesis using hf(3) by(auto intro!: bexI[where x="UNIV"] bexI[where x="β False"] simp: copair_qbs_Mx_def split_beta' comp_def hf(1)) next case 3 then have 4:"f -` {True} â sets real_borel" using measurable_sets[OF hf(2)] by simp have 5:"f -` {True} â {} â§ f -` {True} â UNIV" using 3 by (metis empty_iff imageE insertCI vimage_singleton_eq) have 6:"β True â qbs_Mx X" "β False â qbs_Mx Y" using hf(3)[of True] hf(3)[of False] by(auto simp: 3) show ?thesis apply(simp add: copair_qbs_Mx_def) apply(intro bexI[OF _ 4]) apply(simp add: 5) apply(intro bexI[OF _ 6(1)] bexI[OF _ 6(2)]) apply(auto simp add: hf(1) comp_def) done qed qed next show "case_sum (Pair True) (Pair False) â X <+>â©Q Y ââ©Q (⨿â©Q iâUNIV. if i then X else Y)" proof(rule qbs_morphismI) fix α assume "α â qbs_Mx (X <+>â©Q Y)" then obtain S where hs: "S â sets real_borel" "S = {} â¶ (â α1â qbs_Mx X. α = (λr. Inl (α1 r)))" "S = UNIV â¶ (â α2â qbs_Mx Y. α = (λr. Inr (α2 r)))" "(S â {} â§ S â UNIV) â¶ (â α1â qbs_Mx X. â α2â qbs_Mx Y. α = (λr::real. (if (r â S) then Inl (α1 r) else Inr (α2 r))))" by(auto simp: copair_qbs_Mx_def) consider "S = {}" | "S = UNIV" | "S â {} â§ S â UNIV" by auto thus "case_sum (Pair True) (Pair False) â α â qbs_Mx (⨿â©Q iâUNIV. if i then X else Y)" proof cases case 1 then obtain α1 where ha: "α1â qbs_Mx X" "α = (λr. Inl (α1 r))" using hs(2) by auto hence "case_sum (Pair True) (Pair False) â α = (λr. (True, α1 r))" by auto thus ?thesis by(auto intro!: coprod_qbs_MxI simp: ha) next case 2 then obtain α2 where ha: "α2â qbs_Mx Y" "α = (λr. Inr (α2 r))" using hs(3) by auto hence "case_sum (Pair True) (Pair False) â α = (λr. (False, α2 r))" by auto thus ?thesis by(auto intro!: coprod_qbs_MxI simp: ha) next case 3 then obtain α1 α2 where ha: "α1â qbs_Mx X" "α2â qbs_Mx Y" "α = (λr. (if (r â S) then Inl (α1 r) else Inr (α2 r)))" using hs(4) by auto define f :: "real â bool" where "f â¡ (λr. r â S)" define α' where "α' â¡ (λi. if i then α1 else α2)" have "case_sum (Pair True) (Pair False) â α = (λr. (f r, α' (f r) r))" by(auto simp: f_def α'_def ha(3)) thus ?thesis using hs(1) by(auto intro!: coprod_qbs_MxI simp: ha α'_def f_def) qed qed next show "(λ(b, z). if b then Inl z else Inr z) â case_sum (Pair True) (Pair False) = id" by (auto simp add: sum.case_eq_if ) qed subsubsection â¹ Lists ⺠abbreviation "list_of X ⡠⨿â©Q nâ(UNIV :: nat set). (Î â©Q iâ{..<n}. X)" abbreviation list_nil :: "nat à (nat â 'a)" where "list_nil â¡ (0, λn. undefined)" abbreviation list_cons :: "['a, nat à (nat â 'a)] â nat à (nat â 'a)" where "list_cons x l â¡ (Suc (fst l), (λn. if n = 0 then x else (snd l) (n - 1)))" definition list_head :: "nat à (nat â 'a) â 'a" where "list_head l = snd l 0" definition list_tail :: "nat à (nat â 'a) â nat à (nat â 'a)" where "list_tail l = (fst l - 1, λm. (snd l) (Suc m))" lemma list_simp1: "list_nil â list_cons x l" by simp lemma list_simp2: assumes "list_cons a al = list_cons b bl" shows "a = b" "al = bl" proof - have "a = snd (list_cons a al) 0" "b = snd (list_cons b bl) 0" by auto thus "a = b" by(simp add: assms) next have "fst al = fst bl" using assms by simp moreover have "snd al = snd bl" proof fix n have "snd al n = snd (list_cons a al) (Suc n)" by simp also have "... = snd (list_cons b bl) (Suc n)" by (simp add: assms) also have "... = snd bl n" by simp finally show "snd al n = snd bl n" . qed ultimately show "al = bl" by (simp add: prod.expand) qed lemma list_simp3: shows "list_head (list_cons a l) = a" by(simp add: list_head_def) lemma list_simp4: assumes "l â qbs_space (list_of X)" shows "list_tail (list_cons a l) = l" using assms by(simp_all add: list_tail_def) lemma list_decomp1: assumes "l â qbs_space (list_of X)" shows "l = list_nil ⨠(âa l'. a â qbs_space X â§ l' â qbs_space (list_of X) â§ l = list_cons a l')" proof(cases l) case hl:(Pair n f) show ?thesis proof(cases n) case 0 then show ?thesis using assms hl by simp next case hn:(Suc n') define f' where "f' ⡠λm. f (Suc m)" have "l = list_cons (f 0) (n',f')" proof(simp add: hl hn, standard) fix m show "f m = (if m = 0 then f 0 else snd (n', f') (m - 1))" using assms hl by(cases m; fastforce simp: f'_def) qed moreover have "(n', f') â qbs_space (list_of X)" proof(simp,rule PiE_I) show "âx. x â {..<n'} â¹ f' x â qbs_space X" using assms hl hn by(fastforce simp: f'_def) next fix x assume 1:"x â {..<n'}" thus " f' x = undefined" using hl assms hn by(auto simp: f'_def) qed ultimately show ?thesis using hl assms by(auto intro!: exI[where x="f 0"] exI[where x="(n',λm. if m = 0 then undefined else f (Suc m))"]) qed qed lemma list_simp5: assumes "l â qbs_space (list_of X)" and "l â list_nil" shows "l = list_cons (list_head l) (list_tail l)" proof - obtain a l' where hl: "a â qbs_space X" "l' â qbs_space (list_of X)" "l = list_cons a l'" using list_decomp1[OF assms(1)] assms(2) by blast hence "list_head l = a" "list_tail l = l'" using list_simp3 list_simp4 by auto thus ?thesis using hl(3) list_simp2 by auto qed lemma list_simp6: "list_nil â qbs_space (list_of X)" by simp lemma list_simp7: assumes "a â qbs_space X" and "l â qbs_space (list_of X)" shows "list_cons a l â qbs_space (list_of X)" using assms by(fastforce simp: PiE_def extensional_def) lemma list_destruct_rule: assumes "l â qbs_space (list_of X)" "P list_nil" and "âa l'. a â qbs_space X â¹ l' â qbs_space (list_of X) â¹ P (list_cons a l')" shows "P l" by(rule disjE[OF list_decomp1[OF assms(1)]]) (use assms in auto) lemma list_induct_rule: assumes "l â qbs_space (list_of X)" "P list_nil" and "âa l'. a â qbs_space X â¹ l' â qbs_space (list_of X) â¹ P l' â¹ P (list_cons a l')" shows "P l" proof(cases l) case hl:(Pair n f) then show ?thesis using assms(1) proof(induction n arbitrary: f l) case 0 then show ?case using assms(1,2) by simp next case ih:(Suc n) then obtain a l' where hl: "a â qbs_space X" "l' â qbs_space (list_of X)" "l = list_cons a l'" using list_decomp1 by blast have "P l'" using ih hl(3) by(auto intro!: ih(1)[OF _ hl(2),of "snd l'"]) from assms(3)[OF hl(1,2) this] show ?case by(simp add: hl(3)) qed qed fun from_list :: "'a list â nat à (nat â 'a)" where "from_list [] = list_nil" | "from_list (a#l) = list_cons a (from_list l)" fun to_list' :: "nat â (nat â 'a) â 'a list" where "to_list' 0 _ = []" | "to_list' (Suc n) f = f 0 # to_list' n (λn. f (Suc n))" definition to_list :: "nat à (nat â 'a) â 'a list" where "to_list â¡ case_prod to_list'" lemma to_list_simp1: shows "to_list list_nil = []" by(simp add: to_list_def) lemma to_list_simp2: assumes "l â qbs_space (list_of X)" shows "to_list (list_cons a l) = a # to_list l" using assms by(auto simp:PiE_def to_list_def) lemma from_list_length: "fst (from_list l) = length l" by(induction l, simp_all) lemma from_list_in_list_of: assumes "set l â qbs_space X" shows "from_list l â qbs_space (list_of X)" using assms by(induction l) (auto simp: PiE_def extensional_def Pi_def) lemma from_list_in_list_of': shows "from_list l â qbs_space (list_of (Abs_quasi_borel (UNIV,UNIV)))" proof - have "set l â qbs_space (Abs_quasi_borel (UNIV,UNIV))" by(simp add: qbs_space_def Abs_quasi_borel_inverse[of "(UNIV,UNIV)",simplified is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def,simplified]) thus ?thesis using from_list_in_list_of by blast qed lemma list_cons_in_list_of: assumes "set (a#l) â qbs_space X" shows "list_cons a (from_list l) â qbs_space (list_of X)" using from_list_in_list_of[OF assms] by simp lemma from_list_to_list_ident: "(to_list â from_list) l = l" by(induction l) (simp add: to_list_def,simp add: to_list_simp2[OF from_list_in_list_of']) lemma to_list_from_list_ident: assumes "l â qbs_space (list_of X)" shows "(from_list â to_list) l = l" proof(rule list_induct_rule[OF assms]) fix a l' assume h: "l' â qbs_space (list_of X)" and ih:"(from_list â to_list) l' = l'" show "(from_list â to_list) (list_cons a l') = list_cons a l'" by(auto simp add: to_list_simp2[OF h] ih[simplified]) qed (simp add: to_list_simp1) definition rec_list' :: "'b â ('a â (nat à (nat â 'a)) â 'b â 'b) â (nat à (nat â 'a)) â 'b" where "rec_list' t0 f l â¡ (rec_list t0 (λx l'. f x (from_list l')) (to_list l))" lemma rec_list'_simp1: "rec_list' t f list_nil = t" by(simp add: rec_list'_def to_list_simp1) lemma rec_list'_simp2: assumes "l â qbs_space (list_of X)" shows "rec_list' t f (list_cons x l) = f x l (rec_list' t f l)" by(simp add: rec_list'_def to_list_simp2[OF assms] to_list_from_list_ident[OF assms,simplified]) end
>
Theory Exponent_QuasiBorel
(* Title: Exponent_QuasiBorel.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) subsection â¹Function Spaces⺠theory Exponent_QuasiBorel imports "CoProduct_QuasiBorel" begin subsubsection â¹ Function Spaces ⺠definition exp_qbs_Mx :: "['a quasi_borel, 'b quasi_borel] â (real â 'a => 'b) set" where "exp_qbs_Mx X Y â¡ {g :: real â 'a â 'b. case_prod g â ââ©Q â¨â©Q X ââ©Q Y} " definition exp_qbs :: "['a quasi_borel, 'b quasi_borel] â ('a â 'b) quasi_borel" (infixr "ââ©Q" 61) where "X ââ©Q Y â¡ Abs_quasi_borel (X ââ©Q Y, exp_qbs_Mx X Y)" lemma exp_qbs_f[simp]: "exp_qbs_Mx X Y â UNIV â (X :: 'a quasi_borel) ââ©Q (Y :: 'b quasi_borel)" proof(auto intro!: qbs_morphismI) fix f α r assume h:"f â exp_qbs_Mx X Y" "α â qbs_Mx X" have "f r â α = (λy. case_prod f (r,y)) â α" by auto also have "... â qbs_Mx Y" using qbs_morphism_Pair1'[of r "ââ©Q" "case_prod f" X Y] h by(auto simp: exp_qbs_Mx_def) finally show "f r â α â qbs_Mx Y" . qed lemma exp_qbs_closed1: "qbs_closed1 (exp_qbs_Mx X Y)" proof(rule qbs_closed1I) fix a fix f assume h:"a â exp_qbs_Mx X Y" "f â real_borel ââ©M real_borel" have "a â f = (λr y. case_prod a (f r,y))" by auto moreover have "case_prod ... â ââ©Q â¨â©Q X ââ©Q Y" proof - have "case_prod (λr y. case_prod a (f r,y)) = case_prod a â map_prod f id" by auto also have "... â ââ©Q â¨â©Q X ââ©Q Y" using h by(auto intro!: qbs_morphism_comp qbs_morphism_map_prod simp: exp_qbs_Mx_def) finally show ?thesis . qed ultimately show "a â f â exp_qbs_Mx X Y" by (simp add: exp_qbs_Mx_def) qed lemma exp_qbs_closed2: "qbs_closed2 (X ââ©Q Y) (exp_qbs_Mx X Y)" by(auto intro!: qbs_closed2I qbs_morphism_snd'' simp: exp_qbs_Mx_def split_beta') lemma exp_qbs_closed3:"qbs_closed3 (exp_qbs_Mx X Y)" proof(rule qbs_closed3I) fix P :: "real â nat" fix Fi :: "nat â real â _" assume h:"âi. P -` {i} â sets real_borel" "âi. Fi i â exp_qbs_Mx X Y" show "(λr. Fi (P r) r) â exp_qbs_Mx X Y" unfolding exp_qbs_Mx_def proof(auto intro!: qbs_morphismI) fix α β assume h':"α â pair_qbs_Mx ââ©Q X " have 1:"âi. (λ(r,x). Fi i r x) â α â qbs_Mx Y" using qbs_morphismE(3)[OF h(2)[simplified exp_qbs_Mx_def,simplified]] h' by(simp add: exp_qbs_Mx_def) have 2:"âi. (P â (λr. fst (α r))) -` {i} â sets real_borel" using separate_measurable[OF h(1)] h' by(auto intro!: measurable_separate simp: pair_qbs_Mx_def comp_def) show "(λ(r, y). Fi (P r) r y) â α â qbs_Mx Y" using qbs_closed3_dest[OF 2,of "λi. (λ(r,x). Fi i r x) â α",OF 1] by(simp add: comp_def split_beta') qed qed lemma exp_qbs_correct: "Rep_quasi_borel (exp_qbs X Y) = (X ââ©Q Y, exp_qbs_Mx X Y)" unfolding exp_qbs_def by(auto intro!: Abs_quasi_borel_inverse exp_qbs_f simp: exp_qbs_closed1 exp_qbs_closed2 exp_qbs_closed3) lemma exp_qbs_space[simp]: "qbs_space (exp_qbs X Y) = X ââ©Q Y" by(simp add: qbs_space_def exp_qbs_correct) lemma exp_qbs_Mx[simp]: "qbs_Mx (exp_qbs X Y) = exp_qbs_Mx X Y" by(simp add: qbs_Mx_def exp_qbs_correct) lemma qbs_exp_morphismI: assumes "âα β. α â qbs_Mx X ⹠β â pair_qbs_Mx real_quasi_borel Y â¹ (λ(r,x). (f â α) r x) â β â qbs_Mx Z" shows "f â X ââ©Q exp_qbs Y Z" using assms by(auto intro!: qbs_morphismI simp: exp_qbs_Mx_def comp_def) definition qbs_eval :: "(('a â 'b) à 'a) â 'b" where "qbs_eval a â¡ (fst a) (snd a)" lemma qbs_eval_morphism: "qbs_eval â (exp_qbs X Y) â¨â©Q X ââ©Q Y" proof(rule qbs_morphismI,simp) fix f assume "f â pair_qbs_Mx (exp_qbs X Y) X" let ?f1 = "fst â f" let ?f2 = "snd â f" define g :: "real â real à _" where "g ⡠λr.(r,?f2 r)" have "g â qbs_Mx (real_quasi_borel â¨â©Q X)" proof(auto simp add: pair_qbs_Mx_def) have "fst â g = id" by(auto simp add: g_def comp_def) thus "fst â g â real_borel ââ©M real_borel" by(auto simp add: measurable_ident) next have "snd â g = ?f2" by(auto simp add: g_def) thus "snd â g â qbs_Mx X" using â¹f â pair_qbs_Mx (exp_qbs X Y) X⺠pair_qbs_Mx_def by auto qed moreover have "?f1 â exp_qbs_Mx X Y" using â¹f â pair_qbs_Mx (exp_qbs X Y) X⺠by(simp add: pair_qbs_Mx_def) ultimately have "(λ(r,x). (?f1 r x)) â g â qbs_Mx Y" by (auto simp add: exp_qbs_Mx_def qbs_morphism_def) (metis (mono_tags, lifting) case_prod_conv comp_apply cond_case_prod_eta) moreover have "(λ(r,x). (?f1 r x)) â g = qbs_eval â f" by(auto simp add: case_prod_unfold g_def qbs_eval_def) ultimately show "qbs_eval â f â qbs_Mx Y" by simp qed lemma curry_morphism: "curry â exp_qbs (X â¨â©Q Y) Z ââ©Q exp_qbs X (exp_qbs Y Z)" proof(auto intro!: qbs_morphismI simp: exp_qbs_Mx_def) fix k α α' assume h:"(λ(r, xy). k r xy) â ââ©Q â¨â©Q X â¨â©Q Y ââ©Q Z" "α â pair_qbs_Mx ââ©Q X" "α' â pair_qbs_Mx ââ©Q Y" define β where "β â¡ (λr. (fst (α (fst (α' r))),(snd (α (fst (α' r))), snd (α' r))))" have "(λ(x, y). ((λ(x, y). (curry â k) x y) â α) x y) â α' = (λ(r, xy). k r xy) â β" by(simp add: curry_def split_beta' comp_def β_def) also have "... â qbs_Mx Z" proof - have "β â qbs_Mx (ââ©Q â¨â©Q X â¨â©Q Y)" using h(2,3) qbs_closed1_dest[of _ _ "(λx. fst (α' x))"] by(auto simp: pair_qbs_Mx_def β_def comp_def) thus ?thesis using h by auto qed finally show "(λ(x, y). ((λ(x, y). (curry â k) x y) â α) x y) â α' â qbs_Mx Z" . qed lemma curry_preserves_morphisms: assumes "f â X â¨â©Q Y ââ©Q Z" shows "curry f â X ââ©Q exp_qbs Y Z" by(rule qbs_morphismE(2)[OF curry_morphism,simplified,OF assms]) lemma uncurry_morphism: "case_prod â exp_qbs X (exp_qbs Y Z) ââ©Q exp_qbs (X â¨â©Q Y) Z" proof(auto intro!: qbs_morphismI simp: exp_qbs_Mx_def) fix k α assume h:"(λ(x, y). k x y) â ââ©Q â¨â©Q X ââ©Q exp_qbs Y Z" "α â pair_qbs_Mx ââ©Q (X â¨â©Q Y)" have "(λ(x, y). (case_prod â k) x y) â α = (λ(r,y). k (fst (α r)) (fst (snd (α r))) y) â (λr. (r,snd (snd (α r))))" by(simp add: split_beta' comp_def) also have "... â qbs_Mx Z" proof(rule qbs_morphismE(3)[where X="ââ©Q â¨â©Q Y"]) have "(λr. k (fst (α r)) (fst (snd (α r)))) = (λ(x, y). k x y) â (λr. (fst (α r),fst (snd (α r))))" by auto also have "... â qbs_Mx (exp_qbs Y Z)" apply(rule qbs_morphismE(3)[where X="ââ©Q â¨â©Q X"]) using h(2) by(auto simp: h(1) pair_qbs_Mx_def comp_def) finally show " (λ(r, y). k (fst (α r)) (fst (snd (α r))) y) â ââ©Q â¨â©Q Y ââ©Q Z" by(simp add: exp_qbs_Mx_def) next show "(λr. (r, snd (snd (α r)))) â qbs_Mx (ââ©Q â¨â©Q Y)" using h(2) by(simp add: pair_qbs_Mx_def comp_def) qed finally show "(λ(x, y). (case_prod â k) x y) â α â qbs_Mx Z" . qed lemma uncurry_preserves_morphisms: assumes "f â X ââ©Q exp_qbs Y Z" shows "case_prod f â X â¨â©Q Y ââ©Q Z" by(rule qbs_morphismE(2)[OF uncurry_morphism,simplified,OF assms]) lemma arg_swap_morphism: assumes "f â X ââ©Q exp_qbs Y Z" shows "(λy x. f x y) â Y ââ©Q exp_qbs X Z" using curry_preserves_morphisms[OF qbs_morphism_pair_swap[OF uncurry_preserves_morphisms[OF assms]]] by simp lemma exp_qbs_comp_morphism: assumes "f â W ââ©Q exp_qbs X Y" and "g â W ââ©Q exp_qbs Y Z" shows "(λw. g w â f w) â W ââ©Q exp_qbs X Z" proof(rule qbs_exp_morphismI) fix α β assume h: "α â qbs_Mx W" "β â pair_qbs_Mx ââ©Q X" have "(λ(r, x). ((λw. g w â f w) â α) r x) â β= case_prod g â (λr. ((α â (fst â β)) r, case_prod f ((α â (fst â β)) r, (snd â β) r)))" by(simp add: split_beta' comp_def) also have "... â qbs_Mx Z" proof - have "(λr. ((α â (fst â β)) r, case_prod f ((α â (fst â β)) r, (snd â β) r))) â qbs_Mx (W â¨â©Q Y)" proof(auto simp add: pair_qbs_Mx_def) have "fst â (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r)))) = α â (fst â β)" by (simp add: comp_def) also have "... â qbs_Mx W" using qbs_decomp[of W] h by(simp add: pair_qbs_Mx_def qbs_closed1_def) finally show "fst â (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r)))) â qbs_Mx W" . next have [simp]:"snd â (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r)))) = case_prod f â (λr. ((α â (fst â β)) r, (snd â β) r))" by(simp add: comp_def) have "(λr. ((α â (fst â β)) r, (snd â β) r)) â qbs_Mx (W â¨â©Q X)" proof(auto simp add: pair_qbs_Mx_def) have "fst â (λr. (α (fst (β r)), snd (β r)))= α â (fst â β)" by (simp add: comp_def) also have "... â qbs_Mx W" using qbs_decomp[of W] h by(simp add: pair_qbs_Mx_def qbs_closed1_def) finally show "fst â (λr. (α (fst (β r)), snd (β r))) â qbs_Mx W" . next show "snd â (λr. (α (fst (β r)), snd (β r))) â qbs_Mx X" using h by(simp add: pair_qbs_Mx_def comp_def) qed hence "case_prod f â (λr. ((α â (fst â β)) r, (snd â β) r)) â qbs_Mx Y" using uncurry_preserves_morphisms[OF assms(1)] by auto thus "snd â (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r)))) â qbs_Mx Y" by simp qed thus ?thesis using uncurry_preserves_morphisms[OF assms(2)] by auto qed finally show "(λ(r, x). ((λw. g w â f w) â α) r x) â β â qbs_Mx Z" . qed lemma case_sum_morphism: "case_prod case_sum â exp_qbs X Z â¨â©Q exp_qbs Y Z ââ©Q exp_qbs (X <+>â©Q Y) Z" proof(rule qbs_exp_morphismI) fix α β assume h0:"α â qbs_Mx (exp_qbs X Z â¨â©Q exp_qbs Y Z)" "β â pair_qbs_Mx ââ©Q (X <+>â©Q Y)" let ?α1 = "fst â α" let ?α2 = "snd â α" let ?β1 = "fst â β" let ?β2 = "snd â β" have h:"?α1 â exp_qbs_Mx X Z" "?α2 â exp_qbs_Mx Y Z" "?β1 â real_borel ââ©M real_borel" "?β2 â copair_qbs_Mx X Y" using h0 by (auto simp add: pair_qbs_Mx_def) hence "âSâsets real_borel. (S = {} â¶ (âα1âqbs_Mx X. ?β2 = (λr. Inl (α1 r)))) â§ (S = UNIV â¶ (âα2âqbs_Mx Y. ?β2 = (λr. Inr (α2 r)))) â§ (S â {} â§ S â UNIV â¶ (âα1âqbs_Mx X. âα2âqbs_Mx Y. ?β2 = (λr. if r â S then Inl (α1 r) else Inr (α2 r))))" by(simp add: copair_qbs_Mx_def) then obtain S :: "real set" where hs: "Sâsets real_borel â§ (S = {} â¶ (âα1âqbs_Mx X. ?β2 = (λr. Inl (α1 r)))) â§ (S = UNIV â¶ (âα2âqbs_Mx Y. ?β2 = (λr. Inr (α2 r)))) â§ (S â {} â§ S â UNIV â¶ (âα1âqbs_Mx X. âα2âqbs_Mx Y. ?β2 = (λr. if r â S then Inl (α1 r) else Inr (α2 r))))" by auto show "(λ(r, x). ((λ(x, y). case_sum x y) â α) r x) â β â qbs_Mx Z" proof - have "(λ(r, x). ((λ(x, y). case_sum x y) â α) r x) â β = (λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r))" (is "?lhs = ?rhs") by(auto simp: split_beta' comp_def) (metis comp_apply) also have "... â qbs_Mx Z" (is "?f â _") proof - consider "S = {}" | "S = UNIV" | "S â {} â§ S â UNIV" by auto then show ?thesis proof cases case 1 then obtain α1 where h1: "α1âqbs_Mx X â§ ?β2 = (λr. Inl (α1 r))" using hs by auto then have "(λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r)) = (λr. ?α1 (?β1 r) (α1 r))" by simp also have "... = case_prod ?α1 â (λr. (?β1 r,α1 r))" by auto also have "... â ââ©Q ââ©Q Z" apply(rule qbs_morphism_comp[of _ _ "ââ©Q â¨â©Q X"]) apply(rule qbs_morphism_tuple) using h(3) apply blast using qbs_Mx_is_morphisms h1 apply blast using qbs_Mx_is_morphisms[of "ââ©Q â¨â©Q X"] h(1) by (simp add: exp_qbs_Mx_def) finally show ?thesis using qbs_Mx_is_morphisms by auto next case 2 then obtain α2 where h2: "α2âqbs_Mx Y â§ ?β2 = (λr. Inr (α2 r))" using hs by auto then have "(λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r)) = (λr. ?α2 (?β1 r) (α2 r))" by simp also have "... = case_prod ?α2 â (λr. (?β1 r,α2 r))" by auto also have "... â ââ©Q ââ©Q Z" apply(rule qbs_morphism_comp[of _ _ "ââ©Q â¨â©Q Y"]) apply(rule qbs_morphism_tuple) using h(3) apply blast using qbs_Mx_is_morphisms h2 apply blast using qbs_Mx_is_morphisms[of "ââ©Q â¨â©Q Y"] h(2) by (simp add: exp_qbs_Mx_def) finally show ?thesis using qbs_Mx_is_morphisms by auto next case 3 then obtain α1 α2 where h3: "α1âqbs_Mx X ⧠α2âqbs_Mx Y â§ ?β2 = (λr. if r â S then Inl (α1 r) else Inr (α2 r))" using hs by auto define P :: "real â nat" where "P â¡ (λr. if r â S then 0 else 1)" define γ :: "nat â real â _" where "γ â¡ (λn r. if n = 0 then ?α1 (?β1 r) (α1 r) else ?α2 (?β1 r) (α2 r))" then have "(λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r)) =(λr. γ (P r) r)" by(auto simp add: P_def γ_def h3) also have "... â qbs_Mx Z" proof - have "âi. P -` {i} â sets real_borel" using hs borel_comp[of S] by(simp add: P_def) moreover have"âi. γ i â qbs_Mx Z" proof fix i :: nat consider "i = 0" | "i â 0" by auto then show "γ i â qbs_Mx Z" proof cases case 1 then have "γ i = (λr. ?α1 (?β1 r) (α1 r))" by(simp add: γ_def) also have "... = case_prod ?α1 â (λr. (?β1 r,α1 r))" by auto also have "... â ââ©Q ââ©Q Z" apply(rule qbs_morphism_comp[of _ _ "ââ©Q â¨â©Q X"]) apply(rule qbs_morphism_tuple) using h(3) apply blast using qbs_Mx_is_morphisms h3 apply blast using qbs_Mx_is_morphisms[of "ââ©Q â¨â©Q X"] h(1) by (simp add: exp_qbs_Mx_def) finally show ?thesis using qbs_Mx_is_morphisms by auto next case 2 then have "γ i = (λr. ?α2 (?β1 r) (α2 r))" by(simp add: γ_def) also have "... = case_prod ?α2 â (λr. (?β1 r,α2 r))" by auto also have "... â ââ©Q ââ©Q Z" apply(rule qbs_morphism_comp[of _ _ "ââ©Q â¨â©Q Y"]) apply(rule qbs_morphism_tuple) using h(3) apply blast using qbs_Mx_is_morphisms h3 apply blast using qbs_Mx_is_morphisms[of "ââ©Q â¨â©Q Y"] h(2) by (simp add: exp_qbs_Mx_def) finally show ?thesis using qbs_Mx_is_morphisms by auto qed qed ultimately show ?thesis using qbs_decomp[of Z] by(simp add: qbs_closed3_def) qed finally show ?thesis . qed qed finally show ?thesis . qed qed lemma not_qbs_morphism: "Not â ð¹â©Q ââ©Q ð¹â©Q" by(auto intro!: bool_qbs_morphism) lemma or_qbs_morphism: "(â¨) â ð¹â©Q ââ©Q exp_qbs ð¹â©Q ð¹â©Q" by(auto intro!: bool_qbs_morphism) lemma and_qbs_morphism: "(â§) â ð¹â©Q ââ©Q exp_qbs ð¹â©Q ð¹â©Q" by(auto intro!: bool_qbs_morphism) lemma implies_qbs_morphism: "(â¶) â ð¹â©Q ââ©Q ð¹â©Q ââ©Q ð¹â©Q" by(auto intro!: bool_qbs_morphism) lemma less_nat_qbs_morphism: "(<) â ââ©Q ââ©Q exp_qbs ââ©Q ð¹â©Q" by(auto intro!: nat_qbs_morphism) lemma less_real_qbs_morphism: "(<) â ââ©Q ââ©Q exp_qbs ââ©Q ð¹â©Q" proof(rule curry_preserves_morphisms[where f="(λ(z :: real à real). fst z < snd z)",simplified curry_def,simplified]) have "(λz. fst z < snd z) â real_borel â¨â©M real_borel ââ©M bool_borel" using borel_measurable_pred_less[OF measurable_fst measurable_snd,simplified measurable_cong_sets[OF refl sets_borel_eq_count_space[symmetric],of "borel â¨â©M borel"]] by simp thus "(λz. fst z < snd z) â ââ©Q â¨â©Q ââ©Q ââ©Q ð¹â©Q" by auto qed lemma rec_list_morphism': "rec_list' â qbs_space (exp_qbs Y (exp_qbs (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) (exp_qbs (list_of X) Y)))" apply(simp,rule curry_preserves_morphisms[where f="λyf. rec_list' (fst yf) (snd yf)",simplified curry_def, simplified]) apply(rule arg_swap_morphism) proof(rule coprod_qbs_canonical1') fix n show "(λx y. rec_list' (fst y) (snd y) (n, x)) â (Î â©Q iâ{..<n}. X) ââ©Q exp_qbs (Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y" proof(induction n) case 0 show ?case proof(rule curry_preserves_morphisms[of " (λ(x,y). rec_list' (fst y) (snd y) (0, x))", simplified],rule qbs_morphismI) fix α assume h:"α â qbs_Mx ((Î â©Q iâ{..<0::nat}. X) â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)))" have "âr. fst (α r) = (λn. undefined)" proof - fix r have "âi. (λr. fst (α r) i) = (λr. undefined)" using h by(auto simp: exp_qbs_Mx_def prod_qbs_Mx_def pair_qbs_Mx_def comp_def split_beta') thus "fst (α r) = (λn. undefined)" by(fastforce dest: fun_cong) qed hence "(λ(x, y). rec_list' (fst y) (snd y) (0, x)) â α = (λx. fst (snd (α x)))" by(auto simp: rec_list'_simp1 comp_def split_beta') also have "... â qbs_Mx Y" using h by(auto simp: pair_qbs_Mx_def comp_def) finally show "(λ(x, y). rec_list' (fst y) (snd y) (0, x)) â α â qbs_Mx Y" . qed next case ih:(Suc n) show ?case proof(rule qbs_morphismI) fix α assume h:"α â qbs_Mx (Î â©Q iâ{..<Suc n}. X)" define α' where "α' â¡ (λr. snd (list_tail (Suc n, α r)))" define a where "a â¡ (λr. α r 0)" then have ha:"a â qbs_Mx X" using h by(auto simp: prod_qbs_Mx_def) have 1:"α' â qbs_Mx (Î â©Q iâ{..<n}. X)" using h by(fastforce simp: prod_qbs_Mx_def list_tail_def α'_def) hence 2: "âr. (n, α' r) â qbs_space (list_of X)" using qbs_Mx_to_X[of α'] by fastforce have 3: "âr. (Suc n, α r) â qbs_space (list_of X)" using qbs_Mx_to_X[of α] h by fastforce have 4: "âr. (n, α' r) = list_tail (Suc n, α r)" by(simp add: list_tail_def α'_def) have 5: "âr. (Suc n, α r) = list_cons (a r) (n, α' r)" unfolding a_def by(simp add: list_simp5[OF 3,simplified 4[symmetric],simplified list_head_def]) auto have 6: "(λr. (n, α' r)) â qbs_Mx (list_of X)" using 1 by(auto intro!: coprod_qbs_MxI) have "(λx y. rec_list' (fst y) (snd y) (Suc n, x)) â α = (λr y. rec_list' (fst y) (snd y) (Suc n, α r))" by auto also have "... = (λr y. snd y (a r) (n, α' r) (rec_list' (fst y) (snd y) (n, α' r)))" by(simp only: 5 rec_list'_simp2[OF 2]) also have "... â qbs_Mx (exp_qbs (Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y)" proof - have "(λ(r,y). snd y (a r) (n, α' r) (rec_list' (fst y) (snd y) (n, α' r))) = (λ(y,x1,x2,x3). y x1 x2 x3) â (λ(r,y). (snd y, a r, (n, α' r), rec_list' (fst y) (snd y) (n, α' r)))" by auto also have "... â ââ©Q â¨â©Q (Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) ââ©Q Y" proof(rule qbs_morphism_comp[where Y="exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) â¨â©Q X â¨â©Q list_of X â¨â©Q Y"]) show "(λ(r, y). (snd y, a r, (n, α' r), rec_list' (fst y) (snd y) (n, α' r))) â ââ©Q â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) ââ©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) â¨â©Q X â¨â©Q list_of X â¨â©Q Y" proof(auto simp: split_beta' intro!: qbs_morphism_tuple[OF qbs_morphism_snd''[OF snd_qbs_morphism] qbs_morphism_tuple[of "λ(r, y). a r" "ââ©Q â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))" X], OF _ qbs_morphism_tuple[of "λ(r,y). (n, α' r)"],of "list_of X" "λ(r,y). rec_list' (fst y) (snd y) (n, α' r)",simplified split_beta']) show "(λx. a (fst x)) â ââ©Q â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) ââ©Q X" using ha qbs_Mx_is_morphisms[of X] qbs_morphism_fst''[of a "ââ©Q" X] by auto next show "(λx. (n, α' (fst x))) â ââ©Q â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) ââ©Q list_of X" using qbs_morphism_fst''[of "λr. (n, α' r)" "ââ©Q" "list_of X"] qbs_Mx_is_morphisms[of "list_of X"] 6 by auto next show "(λx. rec_list' (fst (snd x)) (snd (snd x)) (n, α' (fst x))) â ââ©Q â¨â©Q Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) ââ©Q Y" using qbs_morphismE(3)[OF ih 1, simplified comp_def] uncurry_preserves_morphisms[of "(λx y. rec_list' (fst y) (snd y) (n, α' x))" "ââ©Q" "Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))" Y] qbs_Mx_is_morphisms[of "exp_qbs (Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y"] by(fastforce simp: split_beta') qed next show "(λ(y, x1, x2, x3). y x1 x2 x3) â exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) â¨â©Q X â¨â©Q list_of X â¨â©Q Y ââ©Q Y" proof(rule qbs_morphismI) fix β assume "β â qbs_Mx (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) â¨â©Q X â¨â©Q list_of X â¨â©Q Y)" then have "â β1 β2 β3 β4. β = (λr. (β1 r, β2 r, β3 r, β4 r)) ⧠β1 â qbs_Mx (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) ⧠β2 â qbs_Mx X ⧠β3 â qbs_Mx (list_of X) ⧠β4 â qbs_Mx Y" by(auto intro!: exI[where x="fst â β"] exI[where x="fst â snd â β"] exI[where x="fst â snd â snd â β"] exI[where x="snd â snd â snd â β"] simp:pair_qbs_Mx_def comp_def) then obtain β1 β2 β3 β4 where hb: "β = (λr. (β1 r, β2 r, β3 r, β4 r))" "β1 â qbs_Mx (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)))" "β2 â qbs_Mx X" "β3 â qbs_Mx (list_of X)" "β4 â qbs_Mx Y" by auto hence hbq:"(λ(((r,x1),x2),x3). β1 r x1 x2 x3) â ((ââ©Q â¨â©Q X) â¨â©Q list_of X) â¨â©Q Y ââ©Q Y" by(simp add: exp_qbs_Mx_def) (meson uncurry_preserves_morphisms) have "(λ(y, x1, x2, x3). y x1 x2 x3) â β = (λ(((r,x1),x2),x3). β1 r x1 x2 x3) â (λr. (((r,β2 r), β3 r), β4 r))" by(auto simp: hb(1)) also have "... â ââ©Q ââ©Q Y" using hb(2-5) by(auto intro!: qbs_morphism_comp[OF qbs_morphism_tuple[OF qbs_morphism_tuple[OF qbs_morphism_tuple[OF qbs_morphism_ident']]] hbq] simp: qbs_Mx_is_morphisms) finally show "(λ(y, x1, x2, x3). y x1 x2 x3) â β â qbs_Mx Y" by(simp add: qbs_Mx_is_morphisms) qed qed finally show ?thesis by(simp add: exp_qbs_Mx_def) qed finally show "(λx y. rec_list' (fst y) (snd y) (Suc n, x)) â α â qbs_Mx (exp_qbs (Y â¨â©Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y)" . qed qed qed simp end
e>
Theory Probability_Space_QuasiBorel
(* Title: Probability_Space_QuasiBorel.thy Author: Michikazu Hirata, Yasuhiko Minamide, Tokyo Institute of Technology *) section â¹Probability Spaces⺠subsection â¹Probability Measures ⺠theory Probability_Space_QuasiBorel imports Exponent_QuasiBorel begin subsubsection â¹ Probability Measures ⺠type_synonym 'a qbs_prob_t = "'a quasi_borel * (real â 'a) * real measure" locale in_Mx = fixes X :: "'a quasi_borel" and α :: "real â 'a" assumes in_Mx[simp]:"α â qbs_Mx X" locale qbs_prob = in_Mx X α + real_distribution μ for X :: "'a quasi_borel" and α and μ begin declare prob_space_axioms[simp] lemma m_in_space_prob_algebra[simp]: "μ â space (prob_algebra real_borel)" using space_prob_algebra[of real_borel] by simp end locale pair_qbs_probs = qp1:qbs_prob X α μ + qp2:qbs_prob Y β ν for X :: "'a quasi_borel"and α μ and Y :: "'b quasi_borel" and β ν begin sublocale pair_prob_space μ ν by standard lemma ab_measurable[measurable]: "map_prod α β â real_borel â¨â©M real_borel ââ©M qbs_to_measure (X â¨â©Q Y)" using qbs_morphism_map_prod[of α "ââ©Q" X β "ââ©Q" Y] qp1.in_Mx qp2.in_Mx l_preserves_morphisms[of "ââ©Q â¨â©Q ââ©Q" "X â¨â©Q Y"] by(auto simp: qbs_Mx_is_morphisms) lemma ab_g_in_Mx[simp]: "map_prod α β â real_real.g â pair_qbs_Mx X Y" using qbs_closed1_dest[OF qp1.in_Mx] qbs_closed1_dest[OF qp2.in_Mx] by(auto simp add: pair_qbs_Mx_def comp_def) sublocale qbs_prob "X â¨â©Q Y" "map_prod α β â real_real.g" "distr (μ â¨â©M ν) real_borel real_real.f" by(auto simp: qbs_prob_def in_Mx_def) end locale pair_qbs_prob = qp1:qbs_prob X α μ + qp2:qbs_prob Y β ν for X :: "'a quasi_borel"and α μ and Y :: "'a quasi_borel" and β ν begin sublocale pair_qbs_probs by standard lemma same_spaces[simp]: assumes "Y = X" shows "β â qbs_Mx X" by(simp add: assms[symmetric]) end lemma prob_algebra_real_prob_measure: "p â space (prob_algebra (real_borel)) = real_distribution p" proof assume "p â space (prob_algebra real_borel)" then show "real_distribution p" unfolding real_distribution_def real_distribution_axioms_def by(simp add: space_prob_algebra sets_eq_imp_space_eq) next assume "real_distribution p" then interpret rd: real_distribution p . show "p â space (prob_algebra real_borel)" by (simp add: space_prob_algebra rd.prob_space_axioms) qed lemma qbs_probI: assumes "α â qbs_Mx X" and "sets μ = sets borel" and "prob_space μ" shows "qbs_prob X α μ" using assms by(auto intro!: qbs_prob.intro simp: in_Mx_def real_distribution_def real_distribution_axioms_def) lemma qbs_empty_not_qbs_prob :"¬ qbs_prob (empty_quasi_borel) f M" by(simp add: qbs_prob_def in_Mx_def) definition qbs_prob_eq :: "['a qbs_prob_t, 'a qbs_prob_t] â bool" where "qbs_prob_eq p1 p2 â¡ (let (qbs1, a1, m1) = p1; (qbs2, a2, m2) = p2 in qbs_prob qbs1 a1 m1 â§ qbs_prob qbs2 a2 m2 â§ qbs1 = qbs2 â§ distr m1 (qbs_to_measure qbs1) a1 = distr m2 (qbs_to_measure qbs2) a2)" definition qbs_prob_eq2 :: "['a qbs_prob_t, 'a qbs_prob_t] â bool" where "qbs_prob_eq2 p1 p2 â¡ (let (qbs1, a1, m1) = p1; (qbs2, a2, m2) = p2 in qbs_prob qbs1 a1 m1 â§ qbs_prob qbs2 a2 m2 â§ qbs1 = qbs2 â§ (âf â qbs1 ââ©Q real_quasi_borel. (â«x. f (a1 x) â m1) = (â«x. f (a2 x) â m2)))" definition qbs_prob_eq3 :: "['a qbs_prob_t, 'a qbs_prob_t] â bool" where "qbs_prob_eq3 p1 p2 â¡ (let (qbs1, a1, m1) = p1; (qbs2, a2, m2) = p2 in (qbs_prob qbs1 a1 m1 â§ qbs_prob qbs2 a2 m2 â§ qbs1 = qbs2 â§ (âf â qbs1 ââ©Q real_quasi_borel. (â k â qbs_space qbs1. 0 ⤠f k) â¶ (â«x. f (a1 x) â m1) = (â«x. f (a2 x) â m2))))" definition qbs_prob_eq4 :: "['a qbs_prob_t, 'a qbs_prob_t] â bool" where "qbs_prob_eq4 p1 p2 â¡ (let (qbs1, a1, m1) = p1; (qbs2, a2, m2) = p2 in (qbs_prob qbs1 a1 m1 â§ qbs_prob qbs2 a2 m2 â§ qbs1 = qbs2 â§ (âf â qbs1 ââ©Q ââ©Qâ©â¥â©0. (â«â§+x. f (a1 x) â m1) = (â«â§+x. f (a2 x) â m2))))" lemma(in qbs_prob) qbs_prob_eq_refl[simp]: "qbs_prob_eq (X,α,μ) (X,α,μ)" by(simp add: qbs_prob_eq_def qbs_prob_axioms) lemma(in qbs_prob) qbs_prob_eq2_refl[simp]: "qbs_prob_eq2 (X,α,μ) (X,α,μ)" by(simp add: qbs_prob_eq2_def qbs_prob_axioms) lemma(in qbs_prob) qbs_prob_eq3_refl[simp]: "qbs_prob_eq3 (X,α,μ) (X,α,μ)" by(simp add: qbs_prob_eq3_def qbs_prob_axioms) lemma(in qbs_prob) qbs_prob_eq4_refl[simp]: "qbs_prob_eq4 (X,α,μ) (X,α,μ)" by(simp add: qbs_prob_eq4_def qbs_prob_axioms) lemma(in pair_qbs_prob) qbs_prob_eq_intro: assumes "X = Y" and "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β" shows "qbs_prob_eq (X,α,μ) (Y,β,ν)" using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms by(auto simp add: qbs_prob_eq_def) lemma(in pair_qbs_prob) qbs_prob_eq2_intro: assumes "X = Y" and "âf. f â qbs_to_measure X ââ©M real_borel â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)" shows "qbs_prob_eq2 (X,α,μ) (Y,β,ν)" using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms by(auto simp add: qbs_prob_eq2_def) lemma(in pair_qbs_prob) qbs_prob_eq3_intro: assumes "X = Y" and "âf. f â qbs_to_measure X ââ©M real_borel â¹ (â k â qbs_space X. 0 ⤠f k) â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)" shows "qbs_prob_eq3 (X,α,μ) (Y,β,ν)" using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms by(auto simp add: qbs_prob_eq3_def) lemma(in pair_qbs_prob) qbs_prob_eq4_intro: assumes "X = Y" and "âf. f â qbs_to_measure X ââ©M ennreal_borel â¹ (â«â§+x. f (α x) â μ) = (â«â§+x. f (β x) â ν)" shows "qbs_prob_eq4 (X,α,μ) (Y,β,ν)" using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms by(auto simp add: qbs_prob_eq4_def) lemma qbs_prob_eq_dest: assumes "qbs_prob_eq (X,α,μ) (Y,β,ν)" shows "qbs_prob X α μ" "qbs_prob Y β ν" "Y = X" and "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β" using assms by(auto simp: qbs_prob_eq_def) lemma qbs_prob_eq2_dest: assumes "qbs_prob_eq2 (X,α,μ) (Y,β,ν)" shows "qbs_prob X α μ" "qbs_prob Y β ν" "Y = X" and "âf. f â qbs_to_measure X ââ©M real_borel â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)" using assms by(auto simp: qbs_prob_eq2_def) lemma qbs_prob_eq3_dest: assumes "qbs_prob_eq3 (X,α,μ) (Y,β,ν)" shows "qbs_prob X α μ" "qbs_prob Y β ν" "Y = X" and "âf. f â qbs_to_measure X ââ©M real_borel â¹ (â k â qbs_space X. 0 ⤠f k) â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)" using assms by(auto simp: qbs_prob_eq3_def) lemma qbs_prob_eq4_dest: assumes "qbs_prob_eq4 (X,α,μ) (Y,β,ν)" shows "qbs_prob X α μ" "qbs_prob Y β ν" "Y = X" and "âf. f â qbs_to_measure X ââ©M ennreal_borel â¹ (â«â§+x. f (α x) â μ) = (â«â§+x. f (β x) â ν)" using assms by(auto simp: qbs_prob_eq4_def) definition qbs_prob_t_ennintegral :: "['a qbs_prob_t, 'a â ennreal] â ennreal" where "qbs_prob_t_ennintegral p f â¡ (if f â (fst p) ââ©Q ennreal_quasi_borel then (â«â§+x. f (fst (snd p) x) â (snd (snd p))) else 0)" definition qbs_prob_t_integral :: "['a qbs_prob_t, 'a â real] â real" where "qbs_prob_t_integral p f â¡ (if f â (fst p) ââ©Q ââ©Q then (â«x. f (fst (snd p) x) â (snd (snd p))) else 0)" definition qbs_prob_t_integrable :: "['a qbs_prob_t, 'a â real] â bool" where "qbs_prob_t_integrable p f â¡ f â fst p ââ©Q real_quasi_borel â§ integrable (snd (snd p)) (f â (fst (snd p)))" definition qbs_prob_t_measure :: "'a qbs_prob_t â 'a measure" where "qbs_prob_t_measure p â¡ distr (snd (snd p)) (qbs_to_measure (fst p)) (fst (snd p))" lemma qbs_prob_eq_symp: "symp qbs_prob_eq" by(simp add: symp_def qbs_prob_eq_def) lemma qbs_prob_eq_transp: "transp qbs_prob_eq" by(simp add: transp_def qbs_prob_eq_def) quotient_type 'a qbs_prob_space = "'a qbs_prob_t" / partial: qbs_prob_eq morphisms rep_qbs_prob_space qbs_prob_space proof(rule part_equivpI) let ?U = "UNIV :: 'a set" let ?Uf = "UNIV :: (real â 'a) set" let ?f = "(λ_. undefined) :: real â 'a" have "qbs_prob (Abs_quasi_borel (?U,?Uf)) ?f (return borel 0)" proof(auto simp add: qbs_prob_def in_Mx_def) have "Rep_quasi_borel (Abs_quasi_borel (?U,?Uf)) = (?U, ?Uf)" using Abs_quasi_borel_inverse by (auto simp add: qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def) thus "(λ_. undefined) â qbs_Mx (Abs_quasi_borel (?U, ?Uf))" by(simp add: qbs_Mx_def) next show "real_distribution (return borel 0)" by (simp add: prob_space_return real_distribution_axioms_def real_distribution_def) qed thus "âx :: 'a qbs_prob_t . qbs_prob_eq x x" unfolding qbs_prob_eq_def by(auto intro!: exI[where x="(Abs_quasi_borel (?U,?Uf), ?f, return borel 0)"]) qed (simp_all add: qbs_prob_eq_symp qbs_prob_eq_transp) interpretation qbs_prob_space : quot_type "qbs_prob_eq" "Abs_qbs_prob_space" "Rep_qbs_prob_space" using Abs_qbs_prob_space_inverse Rep_qbs_prob_space by(simp add: quot_type_def equivp_implies_part_equivp qbs_prob_space_equivp Rep_qbs_prob_space_inverse Rep_qbs_prob_space_inject) blast lemma qbs_prob_space_induct: assumes "âX α μ. qbs_prob X α μ â¹ P (qbs_prob_space (X,α,μ))" shows "P s" apply(rule qbs_prob_space.abs_induct) using assms by(auto simp: qbs_prob_eq_def) lemma qbs_prob_space_induct': assumes "âX α μ. qbs_prob X α μ â¹ s = qbs_prob_space (X,α,μ)â¹ P (qbs_prob_space (X,α,μ))" shows "P s" by (metis (no_types, lifting) Rep_qbs_prob_space_inverse assms case_prodE qbs_prob_eq_def qbs_prob_space.abs_def qbs_prob_space.rep_prop qbs_prob_space_def) lemma rep_qbs_prob_space: "âX α μ. p = qbs_prob_space (X, α, μ) â§ qbs_prob X α μ" by(rule qbs_prob_space.abs_induct,auto simp add: qbs_prob_eq_def) lemma(in qbs_prob) in_Rep: "(X, α, μ) â Rep_qbs_prob_space (qbs_prob_space (X,α,μ))" by (metis mem_Collect_eq qbs_prob_eq_refl qbs_prob_space.abs_def qbs_prob_space.abs_inverse qbs_prob_space_def) lemma(in qbs_prob) if_in_Rep: assumes "(X',α',μ') â Rep_qbs_prob_space (qbs_prob_space (X,α,μ))" shows "X' = X" "qbs_prob X' α' μ'" "qbs_prob_eq (X,α,μ) (X',α',μ')" proof - have h:"X' = X" by (metis assms mem_Collect_eq qbs_prob_eq_dest(3) qbs_prob_eq_refl qbs_prob_space.abs_def qbs_prob_space.abs_inverse qbs_prob_space_def) have [simp]:"qbs_prob X' α' μ'" by (metis assms mem_Collect_eq prod_cases3 qbs_prob_eq_dest(2) qbs_prob_space.rep_prop) have [simp]:"qbs_prob_eq (X,α,μ) (X',α',μ')" by (metis assms mem_Collect_eq qbs_prob_eq_refl qbs_prob_space.abs_def qbs_prob_space.abs_inverse qbs_prob_space_def) show "X' = X" "qbs_prob X' α' μ'" "qbs_prob_eq (X,α,μ) (X',α',μ')" by simp_all (simp add: h) qed lemma(in qbs_prob) in_Rep_induct: assumes "âY β ν. (Y,β,ν) â Rep_qbs_prob_space (qbs_prob_space (X,α,μ)) â¹ P (Y,β,ν)" shows "P (rep_qbs_prob_space (qbs_prob_space (X,α,μ)))" unfolding rep_qbs_prob_space_def qbs_prob_space.rep_def by(rule someI2[where a="(X,α,μ)"]) (use in_Rep assms in auto) (* qbs_prob_eq[1-4] are equivalent. *) lemma qbs_prob_eq_2_implies_3 : assumes "qbs_prob_eq2 p1 p2" shows "qbs_prob_eq3 p1 p2" using assms by(auto simp: qbs_prob_eq2_def qbs_prob_eq3_def) lemma qbs_prob_eq_3_implies_1 : assumes "qbs_prob_eq3 (p1 :: 'a qbs_prob_t) p2" shows "qbs_prob_eq p1 p2" proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp) fix X Y :: "'a quasi_borel" fix α β μ ν assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)" then have h:"qbs_prob_eq3 (X,α,μ) (Y,β,ν)" using assms by simp then interpret qp : pair_qbs_prob X α μ Y β ν by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq3_def) note [simp] = qbs_prob_eq3_dest(3)[OF h] show "qbs_prob_eq (X,α,μ) (Y,β,ν)" proof(rule qp.qbs_prob_eq_intro) show "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β" proof(rule measure_eqI) fix U assume hu:"U â sets (distr μ (qbs_to_measure X) α)" have "measure (distr μ (qbs_to_measure X) α) U = measure (distr ν (qbs_to_measure X) β) U" (is "?lhs = ?rhs") proof - have "?lhs = measure μ (α -` U â© space μ)" by(rule measure_distr) (use hu in simp_all) also have "... = integralâ§L μ (indicat_real (α -` U))" by simp also have "... = (â«x. indicat_real U (α x) âμ)" using indicator_vimage[of α U] Bochner_Integration.integral_cong[of μ _ "indicat_real (α -` U)" "λx. indicat_real U (α x)"] by auto also have "... = (â«x. indicat_real U (β x) âν)" using qbs_prob_eq3_dest(4)[OF h,of "indicat_real U"] hu by simp also have "... = integralâ§L ν (indicat_real (β -` U))" using indicator_vimage[of β U,symmetric] Bochner_Integration.integral_cong[of ν _ "λx. indicat_real U (β x)" "indicat_real (β -` U)"] by blast also have "... = measure ν (β -` U â© space ν)" by simp also have "... = ?rhs" by(rule measure_distr[symmetric]) (use hu in simp_all) finally show ?thesis . qed thus "emeasure (distr μ (qbs_to_measure X) α) U = emeasure (distr ν (qbs_to_measure X) β) U" using qp.qp2.finite_measure_distr[of β] qp.qp1.finite_measure_distr[of α] by(simp add: finite_measure.emeasure_eq_measure) qed simp qed simp qed lemma qbs_prob_eq_1_implies_2 : assumes "qbs_prob_eq p1 (p2 :: 'a qbs_prob_t)" shows "qbs_prob_eq2 p1 p2" proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp) fix X Y :: "'a quasi_borel" fix α β μ ν assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)" then have h:"qbs_prob_eq (X,α,μ) (Y,β,ν)" using assms by simp then interpret qp : pair_qbs_prob X α μ Y β ν by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq_def) note [simp] = qbs_prob_eq_dest(3)[OF h] show "qbs_prob_eq2 (X,α,μ) (Y,β,ν)" proof(rule qp.qbs_prob_eq2_intro) fix f :: "'a â real" assume [measurable]:"f â borel_measurable (qbs_to_measure X)" show "(â«r. f (α r) â μ) = (â«r. f (β r) â ν)" (is "?lhs = ?rhs") proof - have "?lhs = (â«x. f x â(distr μ (qbs_to_measure X) α))" by(simp add: Bochner_Integration.integral_distr[symmetric]) also have "... = (â«x. f x â(distr ν (qbs_to_measure X) β))" by(simp add: qbs_prob_eq_dest(4)[OF h]) also have "... = ?rhs" by(simp add: Bochner_Integration.integral_distr) finally show ?thesis . qed qed simp qed lemma qbs_prob_eq_1_implies_4 : assumes "qbs_prob_eq p1 p2" shows "qbs_prob_eq4 p1 p2" proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp) fix X Y :: "'a quasi_borel" fix α β μ ν assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)" then have h:"qbs_prob_eq (X,α,μ) (Y,β,ν)" using assms by simp then interpret qp : pair_qbs_prob X α μ Y β ν by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq_def) note [simp] = qbs_prob_eq_dest(3)[OF h] show "qbs_prob_eq4 (X,α,μ) (Y,β,ν)" proof(rule qp.qbs_prob_eq4_intro) fix f ::"'a â ennreal" assume [measurable]:"f â borel_measurable (qbs_to_measure X)" show "(â«â§+ x. f (α x) âμ) = (â«â§+ x. f (β x) âν)" (is "?lhs = ?rhs") proof - have "?lhs = integralâ§N (distr μ (qbs_to_measure X) α) f" by(simp add: nn_integral_distr) also have "... = integralâ§N (distr ν (qbs_to_measure X) β) f" by(simp add: qbs_prob_eq_dest(4)[OF h]) also have "... = ?rhs" by(simp add: nn_integral_distr) finally show ?thesis . qed qed simp qed lemma qbs_prob_eq_4_implies_3 : assumes "qbs_prob_eq4 p1 p2" shows "qbs_prob_eq3 p1 p2" proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp) fix X Y :: "'a quasi_borel" fix α β μ ν assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)" then have h:"qbs_prob_eq4 (X,α,μ) (Y,β,ν)" using assms by simp then interpret qp : pair_qbs_prob X α μ Y β ν by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq4_def) note [simp] = qbs_prob_eq4_dest(3)[OF h] show "qbs_prob_eq3 (X,α,μ) (Y,β,ν)" proof(rule qp.qbs_prob_eq3_intro) fix f :: "'a â real" assume [measurable]:"f â borel_measurable (qbs_to_measure X)" and h': "âkâqbs_space X. 0 ⤠f k" show "(â« x. f (α x) âμ) = (â« x. f (β x) âν)" (is "?lhs = ?rhs") proof - have "?lhs = enn2real (â«â§+ x. ennreal (f (α x)) âμ)" using h' by(auto simp: integral_eq_nn_integral[where f="(λx. f (α x))"] qbs_Mx_to_X(2)) also have "... = enn2real (â«â§+ x. (ennreal â f) (α x) âμ)" by simp also have "... = enn2real (â«â§+ x. (ennreal â f) (β x) âν)" using qbs_prob_eq4_dest(4)[OF h,of "ennreal â f"] by simp also have "... = enn2real (â«â§+ x. ennreal (f (β x)) âν)" by simp also have "... = ?rhs" using h' by(auto simp: integral_eq_nn_integral[where f="(λx. f (β x))"] qbs_Mx_to_X(2)) finally show ?thesis . qed qed simp qed lemma qbs_prob_eq_equiv12 : "qbs_prob_eq = qbs_prob_eq2" using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1 by blast lemma qbs_prob_eq_equiv13 : "qbs_prob_eq = qbs_prob_eq3" using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1 by blast lemma qbs_prob_eq_equiv14 : "qbs_prob_eq = qbs_prob_eq4" using qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1 qbs_prob_eq_1_implies_4 qbs_prob_eq_4_implies_3 qbs_prob_eq_1_implies_2 by blast lemma qbs_prob_eq_equiv23 : "qbs_prob_eq2 = qbs_prob_eq3" using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1 by blast lemma qbs_prob_eq_equiv24 : "qbs_prob_eq2 = qbs_prob_eq4" using qbs_prob_eq_2_implies_3 qbs_prob_eq_4_implies_3 qbs_prob_eq_3_implies_1 qbs_prob_eq_1_implies_4 qbs_prob_eq_1_implies_2 by blast lemma qbs_prob_eq_equiv34: "qbs_prob_eq3 = qbs_prob_eq4" using qbs_prob_eq_3_implies_1 qbs_prob_eq_1_implies_4 qbs_prob_eq_4_implies_3 by blast lemma qbs_prob_eq_equiv31 : "qbs_prob_eq = qbs_prob_eq3" using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1 by blast lemma qbs_prob_space_eq: assumes "qbs_prob_eq (X,α,μ) (Y,β,ν)" shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)" using Quotient3_rel[OF Quotient3_qbs_prob_space] assms by blast lemma(in pair_qbs_prob) qbs_prob_space_eq: assumes "Y = X" and "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β" shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)" using assms qbs_prob_eq_intro qbs_prob_space_eq by auto lemma(in pair_qbs_prob) qbs_prob_space_eq2: assumes "Y = X" and "âf. f â qbs_to_measure X ââ©M real_borel â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)" shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)" using qbs_prob_space_eq assms qbs_prob_eq_2_implies_3[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_eq_3_implies_1[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_eq2_intro qbs_prob_eq_dest(4) by blast lemma(in pair_qbs_prob) qbs_prob_space_eq3: assumes "Y = X" and "âf. f â qbs_to_measure X ââ©M real_borel â¹ (âkâ qbs_space X. 0 ⤠f k) â¹ (â«x. f (α x) â μ) = (â«x. f (β x) â ν)" shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)" using assms qbs_prob_eq_3_implies_1[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_eq3_intro qbs_prob_space_eq qbs_prob_eq_dest(4) by blast lemma(in pair_qbs_prob) qbs_prob_space_eq4: assumes "Y = X" and "âf. f â qbs_to_measure X ââ©M ennreal_borel â¹ (â«â§+x. f (α x) â μ) = (â«â§+x. f (β x) â ν)" shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)" using assms qbs_prob_eq_4_implies_3[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_space_eq3[OF assms(1)] qbs_prob_eq3_dest(4) qbs_prob_eq4_intro by blast lemma(in pair_qbs_prob) qbs_prob_space_eq_inverse: assumes "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)" shows "qbs_prob_eq (X,α,μ) (Y,β,ν)" and "qbs_prob_eq2 (X,α,μ) (Y,β,ν)" and "qbs_prob_eq3 (X,α,μ) (Y,β,ν)" and "qbs_prob_eq4 (X,α,μ) (Y,β,ν)" using Quotient3_rel[OF Quotient3_qbs_prob_space,of "(X, α, μ)" "(Y,β,ν)",simplified] assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms by(simp_all add: qbs_prob_eq_equiv13[symmetric] qbs_prob_eq_equiv12[symmetric] qbs_prob_eq_equiv14[symmetric]) lift_definition qbs_prob_space_qbs :: "'a qbs_prob_space â 'a quasi_borel" is fst by(auto simp add: qbs_prob_eq_def) lemma(in qbs_prob) qbs_prob_space_qbs_computation[simp]: "qbs_prob_space_qbs (qbs_prob_space (X,α,μ)) = X" by(simp add: qbs_prob_space_qbs.abs_eq) lemma rep_qbs_prob_space': assumes "qbs_prob_space_qbs s = X" shows "âα μ. s = qbs_prob_space (X,α,μ) â§ qbs_prob X α μ" proof - obtain X' α μ where hs: "s = qbs_prob_space (X', α, μ)" "qbs_prob X' α μ" using rep_qbs_prob_space[of s] by auto then interpret qp:qbs_prob X' α μ by simp show ?thesis using assms hs(2) by(auto simp add: hs(1)) qed lift_definition qbs_prob_ennintegral :: "['a qbs_prob_space, 'a â ennreal] â ennreal" is qbs_prob_t_ennintegral by(auto simp add: qbs_prob_t_ennintegral_def qbs_prob_eq_equiv14 qbs_prob_eq4_def) lift_definition qbs_prob_integral :: "['a qbs_prob_space, 'a â real] â real" is qbs_prob_t_integral by(auto simp add: qbs_prob_eq_equiv12 qbs_prob_t_integral_def qbs_prob_eq2_def) syntax "_qbs_prob_ennintegral" :: "pttrn â ennreal â 'a qbs_prob_space â ennreal" ("â«â§+â©Q((2 _./ _)/ â_)" [60,61] 110) translations "â«â§+â©Q x. f âp" â "CONST qbs_prob_ennintegral p (λx. f)" syntax "_qbs_prob_integral" :: "pttrn â real â 'a qbs_prob_space â real" ("â«â©Q((2 _./ _)/ â_)" [60,61] 110) translations "â«â©Q x. f âp" â "CONST qbs_prob_integral p (λx. f)" text â¹ We define the function â¹lâ©X â L(P(X)) ââ©M G(X)âº. ⺠lift_definition qbs_prob_measure :: "'a qbs_prob_space â 'a measure" is qbs_prob_t_measure by(auto simp add: qbs_prob_eq_def qbs_prob_t_measure_def) declare [[coercion qbs_prob_measure]] lemma(in qbs_prob) qbs_prob_measure_computation[simp]: "qbs_prob_measure (qbs_prob_space (X,α,μ)) = distr μ (qbs_to_measure X) α" by (simp add: qbs_prob_measure.abs_eq qbs_prob_t_measure_def) definition qbs_emeasure ::"'a qbs_prob_space â 'a set â ennreal" where "qbs_emeasure s â¡ emeasure (qbs_prob_measure s)" lemma(in qbs_prob) qbs_emeasure_computation[simp]: assumes "U â sets (qbs_to_measure X)" shows "qbs_emeasure (qbs_prob_space (X,α,μ)) U = emeasure μ (α -` U)" by(simp add: qbs_emeasure_def emeasure_distr[OF _ assms]) definition qbs_measure ::"'a qbs_prob_space â 'a set â real" where "qbs_measure s â¡ measure (qbs_prob_measure s)"